Documentation Verification Report

HarmonicWave

📁 Source: PhysLean/ClassicalMechanics/WaveEquation/HarmonicWave.lean

Statistics

Metric	Count
Definitions `WaveVector`, `toDirection`, `harmonicWave`, `transverseHarmonicPlaneWave`	4
Theorems `transverseHarmonicPlaneWave_eq_planeWave`	1
Total	5

ClassicalMechanics

Definitions

Name	Category	Theorems
`WaveVector` 📖	CompOp	1 math math: `transverseHarmonicPlaneWave_eq_planeWave`
`harmonicWave` 📖	CompOp	—
`transverseHarmonicPlaneWave` 📖	CompOp	1 math math: `transverseHarmonicPlaneWave_eq_planeWave`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`transverseHarmonicPlaneWave_eq_planeWave` 📖	mathematical	—	`transverseHarmonicPlaneWave` `planeWave` `WaveVector.toDirection` `WaveVector`	—	`harmonicWave.eq_1` `WaveVector.toDirection.eq_1` `Space.basis_repr_inner_eq`

ClassicalMechanics.WaveVector

Definitions

Name	Category	Theorems
`toDirection` 📖	CompOp	1 math math: `ClassicalMechanics.transverseHarmonicPlaneWave_eq_planeWave`

---

← Back to Index