Basic

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

Statistics

Metric	Count
Definitions WaveEquation, planeWave	2
Theorems crossProduct_differentiable_of_right_eq_planewave, crossProduct_time_differentiable_of_right_eq_planewave, planeWave_apply_space_deriv, planeWave_apply_space_deriv_space_deriv, planeWave_differentiable, planeWave_differentiable_space, planeWave_differentiable_time, planeWave_eq, planeWave_laplacian, planeWave_space_deriv, planeWave_space_deriv_space_deriv, planeWave_time_deriv, planeWave_time_deriv_time_deriv, planeWave_waveEquation, space_fderiv_of_inner_product_wave_eq_space_fderiv, time_differentiable_of_eq_planewave, wave_differentiable, wave_dx2, wave_fderiv_inner_eq_inner_fderiv_proj	19
Total	21

ClassicalMechanics

Definitions

Name	Category	Theorems
WaveEquation 📖	MathDef	1 math math: planeWave_waveEquation
planeWave 📖	CompOp	13 math math: planeWave_differentiable_time, transverseHarmonicPlaneWave_eq_planeWave, planeWave_differentiable, planeWave_laplacian, planeWave_space_deriv_space_deriv, planeWave_eq, planeWave_space_deriv, planeWave_waveEquation, planeWave_apply_space_deriv, planeWave_apply_space_deriv_space_deriv, planeWave_differentiable_space, planeWave_time_deriv, planeWave_time_deriv_time_deriv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
crossProduct_differentiable_of_right_eq_planewave 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis Space.Direction.unit	—	crossProduct.eq_1
crossProduct_time_differentiable_of_right_eq_planewave 📖	mathematical	planeWave	Time Time.instAddCommGroup Time.instModuleReal Time.instSeminormedAddCommGroup Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis Space.Direction.unit	—	crossProduct.eq_1 Time.differentiable_euclid Time.val_differentiable
planeWave_apply_space_deriv 📖	mathematical	—	Space.deriv planeWave Space Space.val Space.Direction.unit	—	Space.deriv_eq_fderiv_basis planeWave_differentiable_space planeWave_space_deriv
planeWave_apply_space_deriv_space_deriv 📖	mathematical	—	Space.deriv planeWave Space Space.val Space.Direction.unit	—	planeWave_apply_space_deriv Space.deriv_eq_fderiv_basis planeWave_differentiable_space
planeWave_differentiable 📖	mathematical	—	Time Space Time.instAddCommGroup Space.instAddCommGroup Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Time.instModuleReal Space.instModuleReal Space.instSeminormedAddCommGroup planeWave	—	Time.val_differentiable
planeWave_differentiable_space 📖	mathematical	—	Space Space.instAddCommGroup Space.instModuleReal Space.instSeminormedAddCommGroup planeWave	—	—
planeWave_differentiable_time 📖	mathematical	—	Time Time.instAddCommGroup Time.instModuleReal Time.instSeminormedAddCommGroup planeWave	—	Time.val_differentiable
planeWave_eq 📖	mathematical	—	planeWave Space Space.instInnerReal Space.Direction.unit Time.val	—	—
planeWave_laplacian 📖	mathematical	—	Space.laplacianVec planeWave	—	planeWave_apply_space_deriv_space_deriv Space.direction_unit_sq_sum
planeWave_space_deriv 📖	mathematical	—	Space.deriv planeWave Space Space.val Space.Direction.unit	—	Space.deriv_eq Space.inner_apply_differentiableAt Space.basis_inner
planeWave_space_deriv_space_deriv 📖	mathematical	—	Space.deriv planeWave Space Space.val Space.Direction.unit	—	planeWave_space_deriv Space.deriv_eq_fderiv_basis planeWave_differentiable_space
planeWave_time_deriv 📖	mathematical	—	Time.deriv planeWave Time	—	Time.deriv_eq Time.val_differentiable Time.fderiv_val
planeWave_time_deriv_time_deriv 📖	mathematical	—	Time.deriv planeWave Time	—	planeWave_time_deriv Time.deriv_eq planeWave_differentiable_time
planeWave_waveEquation 📖	mathematical	—	WaveEquation planeWave	—	WaveEquation.eq_1 planeWave_laplacian planeWave_time_deriv_time_deriv
space_fderiv_of_inner_product_wave_eq_space_fderiv 📖	mathematical	—	Space.val Space.Direction.unit Time.deriv Space Space.instInnerReal Time.val	—	Space.deriv_eq_fderiv_basis planeWave_apply_space_deriv planeWave_time_deriv
time_differentiable_of_eq_planewave 📖	mathematical	planeWave	Time Time.instAddCommGroup Time.instModuleReal Time.instSeminormedAddCommGroup	—	Time.val_differentiable
wave_differentiable 📖	mathematical	—	Space Space.instAddCommGroup Space.instModuleReal Space.instSeminormedAddCommGroup Space.instInnerReal Space.Direction.unit	—	—
wave_dx2 📖	mathematical	—	Space Space.instSeminormedAddCommGroup Space.instAddCommGroup Space.instModuleReal Space.instInnerReal Space.Direction.unit Space.val Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	wave_differentiable Space.inner_apply_differentiableAt Space.basis_inner
wave_fderiv_inner_eq_inner_fderiv_proj 📖	mathematical	—	Space.val Space.Direction.unit Space Space.instSeminormedAddCommGroup Space.instAddCommGroup Space.instModuleReal Space.instInnerReal Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	Space.inner_apply_differentiableAt Space.basis_inner

---

← Back to Index