Documentation Verification Report

Solution

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

Statistics

Metric	Count
Definitions `InitialConditions`, `instZero`, `trajectory`, `v₀`, `x₀`, `InitialConditionsAtTime`, `toInitialConditions`, `t₀`, `v_t₀`, `x_t₀`	10
Theorems `ext`, `ext_iff`, `tan_time_eq_of_trajectory_velocity_eq_zero`, `trajectories_unique`, `trajectory_acceleration`, `trajectory_contDiff`, `trajectory_energy`, `trajectory_eq`, `trajectory_equationOfMotion`, `trajectory_position_at_zero`, `trajectory_velocity`, `trajectory_velocity_at_zero`, `trajectory_velocity_eq_zero_at_arctan`, `trajectory_velocity_eq_zero_iff`, `trajectory_zero`, `v₀_zero`, `x₀_zero`, `ext`, `ext_iff`, `toInitialConditions_energy_at_t₀`, `toInitialConditions_trajectory_at_t₀`, `toInitialConditions_velocity_at_t₀`	22
Total	32

ClassicalMechanics.HarmonicOscillator

Definitions

Name	Category	Theorems
`InitialConditions` 📖	CompData	3 math math: `InitialConditions.x₀_zero`, `InitialConditions.trajectory_zero`, `InitialConditions.v₀_zero`
`InitialConditionsAtTime` 📖	CompData	—

ClassicalMechanics.HarmonicOscillator.InitialConditions

Definitions

Name	Category	Theorems
`instZero` 📖	CompOp	3 math math: `x₀_zero`, `trajectory_zero`, `v₀_zero`
`trajectory` 📖	CompOp	15 math math: `trajectory_velocity_eq_zero_at_arctan`, `trajectory_velocity_eq_zero_iff`, `trajectory_velocity`, `trajectories_unique`, `trajectory_position_at_zero`, `trajectory_equationOfMotion`, `trajectory_eq`, `trajectory_zero`, `trajectory_energy`, `ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions_energy_at_t₀`, `ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions_velocity_at_t₀`, `trajectory_acceleration`, `trajectory_contDiff`, `ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions_trajectory_at_t₀`, `trajectory_velocity_at_zero`
`v₀` 📖	CompOp	10 math math: `ext_iff`, `tan_time_eq_of_trajectory_velocity_eq_zero`, `trajectory_velocity_eq_zero_at_arctan`, `trajectory_velocity_eq_zero_iff`, `trajectory_velocity`, `trajectory_eq`, `trajectory_energy`, `trajectory_acceleration`, `v₀_zero`, `trajectory_velocity_at_zero`
`x₀` 📖	CompOp	10 math math: `ext_iff`, `x₀_zero`, `tan_time_eq_of_trajectory_velocity_eq_zero`, `trajectory_velocity_eq_zero_at_arctan`, `trajectory_velocity_eq_zero_iff`, `trajectory_velocity`, `trajectory_position_at_zero`, `trajectory_eq`, `trajectory_energy`, `trajectory_acceleration`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`x₀` `v₀`	—	—	—
`ext_iff` 📖	mathematical	—	`x₀` `v₀`	—	`ext`
`tan_time_eq_of_trajectory_velocity_eq_zero` 📖	mathematical	`Time.deriv` `trajectory`	`ClassicalMechanics.HarmonicOscillator.ω` `Time.val` `v₀` `x₀`	—	`ClassicalMechanics.HarmonicOscillator.ω_neq_zero` `trajectory_velocity`
`trajectories_unique` 📖	mathematical	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `ClassicalMechanics.HarmonicOscillator.EquationOfMotion` `Time.instOfNat` `x₀` `Time.deriv` `v₀`	`trajectory`	—	`ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_newtons_2nd_law` `trajectory_contDiff` `trajectory_equationOfMotion` `Time.deriv.eq_1` `Time.deriv_differentiable_of_contDiff` `ClassicalMechanics.HarmonicOscillator.force_eq_linear` `trajectory_position_at_zero` `trajectory_velocity_at_zero` `ClassicalMechanics.HarmonicOscillator.energy_conservation_of_equationOfMotion'` `ClassicalMechanics.HarmonicOscillator.m_pos` `ClassicalMechanics.HarmonicOscillator.k_pos` `ClassicalMechanics.HarmonicOscillator.k_neq_zero`
`trajectory_acceleration` 📖	mathematical	—	`Time.deriv` `trajectory` `ClassicalMechanics.HarmonicOscillator.ω` `Time.val` `x₀` `v₀`	—	`trajectory_velocity` `Time.deriv.eq_1` `Time.val_differentiable` `Time.fderiv_val`
`trajectory_contDiff` 📖	mathematical	—	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `trajectory`	—	`trajectory_eq`
`trajectory_energy` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.energy` `trajectory` `ClassicalMechanics.HarmonicOscillator.m` `v₀` `ClassicalMechanics.HarmonicOscillator.k` `x₀`	—	`ClassicalMechanics.HarmonicOscillator.energy_conservation_of_equationOfMotion'` `trajectory_contDiff` `trajectory_equationOfMotion` `trajectory_velocity_at_zero` `trajectory_position_at_zero`
`trajectory_eq` 📖	mathematical	—	`trajectory` `ClassicalMechanics.HarmonicOscillator.ω` `Time.val` `x₀` `v₀`	—	—
`trajectory_equationOfMotion` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.EquationOfMotion` `trajectory`	—	`ClassicalMechanics.HarmonicOscillator.EquationOfMotion.eq_1` `ClassicalMechanics.HarmonicOscillator.gradLagrangian_eq_force` `trajectory_contDiff` `trajectory_acceleration` `ClassicalMechanics.HarmonicOscillator.force_eq_linear` `ClassicalMechanics.HarmonicOscillator.ω_sq` `ClassicalMechanics.HarmonicOscillator.ω_neq_zero`
`trajectory_position_at_zero` 📖	mathematical	—	`trajectory` `Time` `Time.instOfNat` `x₀`	—	`Time.zero_val`
`trajectory_velocity` 📖	mathematical	—	`Time.deriv` `trajectory` `ClassicalMechanics.HarmonicOscillator.ω` `Time.val` `x₀` `v₀`	—	`trajectory_eq` `Time.deriv.eq_1` `Time.val_differentiable` `Time.fderiv_val` `ClassicalMechanics.HarmonicOscillator.ω_neq_zero`
`trajectory_velocity_at_zero` 📖	mathematical	—	`Time.deriv` `trajectory` `Time` `Time.instOfNat` `v₀`	—	`trajectory_velocity` `Time.zero_val`
`trajectory_velocity_eq_zero_at_arctan` 📖	mathematical	—	`Time.deriv` `trajectory` `v₀` `ClassicalMechanics.HarmonicOscillator.ω` `x₀`	—	`trajectory_velocity` `ClassicalMechanics.HarmonicOscillator.ω_neq_zero`
`trajectory_velocity_eq_zero_iff` 📖	mathematical	—	`Time.deriv` `trajectory` `x₀` `v₀` `ClassicalMechanics.HarmonicOscillator.ω`	—	`ClassicalMechanics.HarmonicOscillator.energy_eq` `trajectory_energy` `ClassicalMechanics.HarmonicOscillator.ω_sq` `ClassicalMechanics.HarmonicOscillator.kineticEnergy_eq` `ClassicalMechanics.HarmonicOscillator.potentialEnergy_eq` `ClassicalMechanics.HarmonicOscillator.k_neq_zero` `ClassicalMechanics.HarmonicOscillator.inverse_ω_sq` `ClassicalMechanics.HarmonicOscillator.ω_neq_zero`
`trajectory_zero` 📖	mathematical	—	`trajectory` `ClassicalMechanics.HarmonicOscillator.InitialConditions` `instZero`	—	—
`v₀_zero` 📖	mathematical	—	`v₀` `ClassicalMechanics.HarmonicOscillator.InitialConditions` `instZero`	—	—
`x₀_zero` 📖	mathematical	—	`x₀` `ClassicalMechanics.HarmonicOscillator.InitialConditions` `instZero`	—	—

ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime

Definitions

Name	Category	Theorems
`toInitialConditions` 📖	CompOp	3 math math: `toInitialConditions_energy_at_t₀`, `toInitialConditions_velocity_at_t₀`, `toInitialConditions_trajectory_at_t₀`
`t₀` 📖	CompOp	4 math math: `ext_iff`, `toInitialConditions_energy_at_t₀`, `toInitialConditions_velocity_at_t₀`, `toInitialConditions_trajectory_at_t₀`
`v_t₀` 📖	CompOp	3 math math: `ext_iff`, `toInitialConditions_energy_at_t₀`, `toInitialConditions_velocity_at_t₀`
`x_t₀` 📖	CompOp	3 math math: `ext_iff`, `toInitialConditions_energy_at_t₀`, `toInitialConditions_trajectory_at_t₀`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`t₀` `x_t₀` `v_t₀`	—	—	—
`ext_iff` 📖	mathematical	—	`t₀` `x_t₀` `v_t₀`	—	`ext`
`toInitialConditions_energy_at_t₀` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.energy` `ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory` `toInitialConditions` `t₀` `ClassicalMechanics.HarmonicOscillator.m` `v_t₀` `ClassicalMechanics.HarmonicOscillator.k` `x_t₀`	—	`toInitialConditions_velocity_at_t₀` `toInitialConditions_trajectory_at_t₀`
`toInitialConditions_trajectory_at_t₀` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory` `toInitialConditions` `t₀` `x_t₀`	—	`ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_eq` `toInitialConditions.eq_1` `ClassicalMechanics.HarmonicOscillator.ω_neq_zero`
`toInitialConditions_velocity_at_t₀` 📖	mathematical	—	`Time.deriv` `ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory` `toInitialConditions` `t₀` `v_t₀`	—	`ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity` `toInitialConditions.eq_1` `ClassicalMechanics.HarmonicOscillator.ω_neq_zero`

---

← Back to Index