Basic

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

Statistics

Metric	Count
Definitions `HarmonicOscillator`, `EquationOfMotion`, `energy`, `force`, `gradLagrangian`, `hamiltonEqOp`, `hamiltonian`, `k`, `kineticEnergy`, `lagrangian`, `m`, `potentialEnergy`, `toCanonicalMomentum`, `ω`	14
Theorems `contDiff_lagrangian`, `energy_conservation_of_equationOfMotion`, `energy_conservation_of_equationOfMotion'`, `energy_deriv`, `energy_differentiable`, `energy_eq`, `equationOfMotion_iff_gradLagrangian_zero`, `equationOfMotion_iff_hamiltonEqOp_eq_zero`, `equationOfMotion_iff_newtons_2nd_law`, `equationOfMotion_tfae`, `force_eq_linear`, `gradLagrangian_eq_eulerLagrangeOp`, `gradLagrangian_eq_force`, `gradient_hamiltonian_momentum_eq`, `gradient_hamiltonian_position_eq`, `gradient_lagrangian_position_eq`, `gradient_lagrangian_velocity_eq`, `hamiltonian_contDiff`, `hamiltonian_eq`, `hamiltonian_eq_energy`, `inverse_ω_sq`, `k_neq_zero`, `k_pos`, `kineticEnergy_deriv`, `kineticEnergy_differentiable`, `kineticEnergy_eq`, `lagrangian_eq`, `lagrangian_eq_kineticEnergy_sub_potentialEnergy`, `m_neq_zero`, `m_pos`, `potentialEnergy_deriv`, `potentialEnergy_differentiable`, `potentialEnergy_eq`, `toCanonicalMomentum_eq`, `ω_neq_zero`, `ω_pos`, `ω_sq`	37
Total	51

ClassicalMechanics

Definitions

Name	Category	Theorems
`HarmonicOscillator` 📖	CompData	—

ClassicalMechanics.HarmonicOscillator

Definitions

Name	Category	Theorems
`EquationOfMotion` 📖	MathDef	5 math math: `equationOfMotion_iff_gradLagrangian_zero`, `equationOfMotion_iff_hamiltonEqOp_eq_zero`, `equationOfMotion_iff_newtons_2nd_law`, `InitialConditions.trajectory_equationOfMotion`, `equationOfMotion_tfae`
`energy` 📖	CompOp	8 math math: `hamiltonian_eq_energy`, `energy_conservation_of_equationOfMotion'`, `energy_differentiable`, `energy_eq`, `energy_deriv`, `InitialConditions.trajectory_energy`, `InitialConditionsAtTime.toInitialConditions_energy_at_t₀`, `energy_conservation_of_equationOfMotion`
`force` 📖	CompOp	3 math math: `gradLagrangian_eq_force`, `equationOfMotion_iff_newtons_2nd_law`, `force_eq_linear`
`gradLagrangian` 📖	CompOp	3 math math: `equationOfMotion_iff_gradLagrangian_zero`, `gradLagrangian_eq_force`, `gradLagrangian_eq_eulerLagrangeOp`
`hamiltonEqOp` 📖	CompOp	2 math math: `equationOfMotion_iff_hamiltonEqOp_eq_zero`, `equationOfMotion_tfae`
`hamiltonian` 📖	CompOp	6 math math: `hamiltonian_eq_energy`, `hamiltonian_eq`, `gradient_hamiltonian_momentum_eq`, `hamiltonian_contDiff`, `gradient_hamiltonian_position_eq`, `equationOfMotion_tfae`
`k` 📖	CompOp	13 math math: `inverse_ω_sq`, `hamiltonian_eq`, `ω_sq`, `gradient_hamiltonian_position_eq`, `potentialEnergy_deriv`, `force_eq_linear`, `lagrangian_eq`, `gradient_lagrangian_position_eq`, `k_pos`, `energy_deriv`, `InitialConditions.trajectory_energy`, `InitialConditionsAtTime.toInitialConditions_energy_at_t₀`, `potentialEnergy_eq`
`kineticEnergy` 📖	CompOp	5 math math: `kineticEnergy_eq`, `kineticEnergy_differentiable`, `energy_eq`, `kineticEnergy_deriv`, `lagrangian_eq_kineticEnergy_sub_potentialEnergy`
`lagrangian` 📖	CompOp	7 math math: `contDiff_lagrangian`, `gradLagrangian_eq_eulerLagrangeOp`, `gradient_lagrangian_velocity_eq`, `lagrangian_eq`, `gradient_lagrangian_position_eq`, `equationOfMotion_tfae`, `lagrangian_eq_kineticEnergy_sub_potentialEnergy`
`m` 📖	CompOp	15 math math: `inverse_ω_sq`, `hamiltonian_eq`, `kineticEnergy_eq`, `toCanonicalMomentum_eq`, `gradient_hamiltonian_momentum_eq`, `ω_sq`, `gradLagrangian_eq_force`, `gradient_lagrangian_velocity_eq`, `equationOfMotion_iff_newtons_2nd_law`, `lagrangian_eq`, `kineticEnergy_deriv`, `energy_deriv`, `InitialConditions.trajectory_energy`, `InitialConditionsAtTime.toInitialConditions_energy_at_t₀`, `m_pos`
`potentialEnergy` 📖	CompOp	5 math math: `potentialEnergy_deriv`, `energy_eq`, `lagrangian_eq_kineticEnergy_sub_potentialEnergy`, `potentialEnergy_eq`, `potentialEnergy_differentiable`
`toCanonicalMomentum` 📖	CompOp	4 math math: `hamiltonian_eq_energy`, `toCanonicalMomentum_eq`, `equationOfMotion_iff_hamiltonEqOp_eq_zero`, `equationOfMotion_tfae`
`ω` 📖	CompOp	9 math math: `inverse_ω_sq`, `InitialConditions.tan_time_eq_of_trajectory_velocity_eq_zero`, `InitialConditions.trajectory_velocity_eq_zero_at_arctan`, `InitialConditions.trajectory_velocity_eq_zero_iff`, `ω_sq`, `InitialConditions.trajectory_velocity`, `ω_pos`, `InitialConditions.trajectory_eq`, `InitialConditions.trajectory_acceleration`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff_lagrangian` 📖	mathematical	—	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `lagrangian`	—	`lagrangian_eq` `ContDiff.inner'`
`energy_conservation_of_equationOfMotion` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `EquationOfMotion`	`Time.deriv` `energy`	—	`energy_deriv` `equationOfMotion_iff_newtons_2nd_law` `force_eq_linear`
`energy_conservation_of_equationOfMotion'` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `EquationOfMotion`	`energy` `Time.instOfNat`	—	`energy_conservation_of_equationOfMotion` `energy_differentiable` `Time.ext` `Time.one_val`
`energy_deriv` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`Time.deriv` `energy` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `m` `k`	—	`Time.deriv_eq` `kineticEnergy_differentiable` `potentialEnergy_differentiable` `potentialEnergy_deriv` `kineticEnergy_deriv`
`energy_differentiable` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `energy`	—	`energy_eq` `kineticEnergy_differentiable` `potentialEnergy_differentiable`
`energy_eq` 📖	mathematical	—	`energy` `kineticEnergy` `potentialEnergy`	—	—
`equationOfMotion_iff_gradLagrangian_zero` 📖	mathematical	—	`EquationOfMotion` `gradLagrangian` `Time`	—	—
`equationOfMotion_iff_hamiltonEqOp_eq_zero` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`EquationOfMotion` `hamiltonEqOp` `toCanonicalMomentum` `Time.deriv`	—	`hamiltonEqOp.eq_1` `ClassicalMechanics.hamiltonEqOp_eq_zero_iff_hamiltons_equations` `gradient.congr_simp` `toCanonicalMomentum_eq` `gradient_hamiltonian_momentum_eq` `gradient_hamiltonian_position_eq` `equationOfMotion_iff_newtons_2nd_law` `Time.deriv_smul` `Time.deriv_differentiable_of_contDiff` `force_eq_linear`
`equationOfMotion_iff_newtons_2nd_law` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`EquationOfMotion` `m` `Time.deriv` `force`	—	`EquationOfMotion.eq_1` `gradLagrangian_eq_force`
`equationOfMotion_tfae` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`EquationOfMotion` `hamiltonEqOp` `toCanonicalMomentum` `Time.deriv` `varGradient` `Time.instInnerProductSpaceReal` `Time.instFiniteDimensionalReal` `Time.instMeasurableSpace` `Time.instBorelSpace` `instInnerProductSpace'` `lagrangian` `Time.instSeminormedAddCommGroup` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instOfNat` `instInnerProductSpace'Prod` `instInnerOfInnerProductSpace'` `hamiltonian`	—	`Time.instFiniteDimensionalReal` `Time.instBorelSpace` `equationOfMotion_iff_hamiltonEqOp_eq_zero` `equationOfMotion_iff_newtons_2nd_law` `ClassicalMechanics.hamiltons_equations_varGradient` `toCanonicalMomentum_eq` `Time.deriv_contDiff_of_contDiff` `hamiltonian_contDiff` `ClassicalMechanics.euler_lagrange_varGradient` `contDiff_lagrangian` `gradLagrangian_eq_eulerLagrangeOp` `equationOfMotion_iff_gradLagrangian_zero`
`force_eq_linear` 📖	mathematical	—	`force` `k`	—	`DifferentiableAt.inner'`
`gradLagrangian_eq_eulerLagrangeOp` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`gradLagrangian` `ClassicalMechanics.eulerLagrangeOp` `lagrangian`	—	`Time.instFiniteDimensionalReal` `Time.instBorelSpace` `gradLagrangian.eq_1` `ClassicalMechanics.euler_lagrange_varGradient` `contDiff_lagrangian`
`gradLagrangian_eq_force` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`gradLagrangian` `force` `m` `Time.deriv`	—	`gradLagrangian_eq_eulerLagrangeOp` `ClassicalMechanics.eulerLagrangeOp.eq_1` `gradient.congr_simp` `lagrangian_eq` `Space.euclid_gradient_eq_sum` `DifferentiableAt.inner'` `force_eq_linear` `Time.deriv_smul` `Time.deriv_differentiable_of_contDiff` `gradient_lagrangian_velocity_eq`
`gradient_hamiltonian_momentum_eq` 📖	mathematical	—	`hamiltonian` `m`	—	`hamiltonian_eq` `gradient.congr_simp` `Space.euclid_gradient_eq_sum` `DifferentiableAt.inner'`
`gradient_hamiltonian_position_eq` 📖	mathematical	—	`hamiltonian` `k`	—	`hamiltonian_eq` `gradient.congr_simp` `Space.euclid_gradient_eq_sum` `DifferentiableAt.inner'`
`gradient_lagrangian_position_eq` 📖	mathematical	—	`lagrangian` `k`	—	`gradient.congr_simp` `lagrangian_eq` `Space.euclid_gradient_eq_sum` `DifferentiableAt.inner'`
`gradient_lagrangian_velocity_eq` 📖	mathematical	—	`lagrangian` `m`	—	`gradient.congr_simp` `lagrangian_eq` `Space.euclid_gradient_eq_sum` `DifferentiableAt.inner'`
`hamiltonian_contDiff` 📖	mathematical	—	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `hamiltonian`	—	`hamiltonian_eq` `ContDiff.inner'`
`hamiltonian_eq` 📖	mathematical	—	`hamiltonian` `m` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `k`	—	`gradient.congr_simp` `lagrangian_eq` `m_neq_zero`
`hamiltonian_eq_energy` 📖	mathematical	—	`hamiltonian` `toCanonicalMomentum` `Time.deriv` `energy`	—	`hamiltonian.eq_1` `toCanonicalMomentum_eq`
`inverse_ω_sq` 📖	mathematical	—	`ω` `m` `k`	—	`ω_sq`
`k_neq_zero` 📖	—	—	—	—	`k_pos`
`k_pos` 📖	mathematical	—	`k`	—	—
`kineticEnergy_deriv` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`Time.deriv` `kineticEnergy` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `m`	—	`DifferentiableAt.inner'` `Time.deriv_differentiable_of_contDiff` `Time.deriv.eq_1`
`kineticEnergy_differentiable` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `kineticEnergy`	—	`kineticEnergy_eq` `ContDiff.inner'` `Time.deriv_differentiable_of_contDiff`
`kineticEnergy_eq` 📖	mathematical	—	`kineticEnergy` `m` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `Time.deriv`	—	—
`lagrangian_eq` 📖	mathematical	—	`lagrangian` `m` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `k`	—	—
`lagrangian_eq_kineticEnergy_sub_potentialEnergy` 📖	mathematical	—	`lagrangian` `Time.deriv` `kineticEnergy` `potentialEnergy`	—	`lagrangian_eq` `kineticEnergy.eq_1` `potentialEnergy.eq_1`
`m_neq_zero` 📖	—	—	—	—	`m_pos`
`m_pos` 📖	mathematical	—	`m`	—	—
`potentialEnergy_deriv` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`Time.deriv` `potentialEnergy` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `k`	—	`DifferentiableAt.inner'` `Time.deriv.eq_1`
`potentialEnergy_differentiable` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `potentialEnergy`	—	`potentialEnergy_eq` `ContDiff.inner'`
`potentialEnergy_eq` 📖	mathematical	—	`potentialEnergy` `k` `instInnerOfInnerProductSpace'` `instInnerProductSpace'`	—	—
`toCanonicalMomentum_eq` 📖	mathematical	—	`toCanonicalMomentum` `m`	—	`gradient_lagrangian_velocity_eq`
`ω_neq_zero` 📖	—	—	—	—	`ω_pos`
`ω_pos` 📖	mathematical	—	`ω`	—	`k_pos` `m_pos`
`ω_sq` 📖	mathematical	—	`ω` `k` `m`	—	`ω.eq_1` `k_pos` `m_pos`

---

← Back to Index