Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `DampedHarmonicOscillator`, `EquationOfMotion`, `IsCriticallyDamped`, `IsOverdamped`, `IsUnderdamped`, `discriminant`, `energy`, `energyDissipationRate`, `k`, `kineticEnergy`, `m`, `potentialEnergy`, `γ`, `ω₀`	14
Theorems `energy_dissipation_rate`, `energy_not_conserved`, `k_ne_zero`, `k_pos`, `kineticEnergy_eq`, `m_ne_zero`, `m_pos`, `potentialEnergy_eq`, `γ_nonneg`, `ω₀_pos`, `ω₀_sq`	11
Total	25

ClassicalMechanics

Definitions

Name	Category	Theorems
`DampedHarmonicOscillator` 📖	CompData	—

ClassicalMechanics.DampedHarmonicOscillator

Definitions

Name	Category	Theorems
`EquationOfMotion` 📖	MathDef	—
`IsCriticallyDamped` 📖	MathDef	—
`IsOverdamped` 📖	MathDef	—
`IsUnderdamped` 📖	MathDef	—
`discriminant` 📖	CompOp	—
`energy` 📖	CompOp	2 math math: `energy_not_conserved`, `energy_dissipation_rate`
`energyDissipationRate` 📖	CompOp	—
`k` 📖	CompOp	3 math math: `k_pos`, `potentialEnergy_eq`, `ω₀_sq`
`kineticEnergy` 📖	CompOp	1 math math: `kineticEnergy_eq`
`m` 📖	CompOp	3 math math: `kineticEnergy_eq`, `m_pos`, `ω₀_sq`
`potentialEnergy` 📖	CompOp	1 math math: `potentialEnergy_eq`
`γ` 📖	CompOp	2 math math: `γ_nonneg`, `energy_dissipation_rate`
`ω₀` 📖	CompOp	2 math math: `ω₀_pos`, `ω₀_sq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`energy_dissipation_rate` 📖	mathematical	`EquationOfMotion` `Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal`	`Time.deriv` `energy` `γ`	—	`energy.eq_1` `kineticEnergy_eq` `potentialEnergy_eq` `Time.deriv_eq` `Time.deriv_differentiable_of_contDiff` `Time.deriv.eq_1`
`energy_not_conserved` 📖	mathematical	`EquationOfMotion` `Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `γ`	`Time.deriv` `energy`	—	`energy_dissipation_rate`
`k_ne_zero` 📖	—	—	—	—	`k_pos`
`k_pos` 📖	mathematical	—	`k`	—	—
`kineticEnergy_eq` 📖	mathematical	—	`kineticEnergy` `m` `Time.deriv`	—	—
`m_ne_zero` 📖	—	—	—	—	`m_pos`
`m_pos` 📖	mathematical	—	`m`	—	—
`potentialEnergy_eq` 📖	mathematical	—	`potentialEnergy` `k`	—	—
`γ_nonneg` 📖	mathematical	—	`γ`	—	—
`ω₀_pos` 📖	mathematical	—	`ω₀`	—	`k_pos` `m_pos`
`ω₀_sq` 📖	mathematical	—	`ω₀` `k` `m`	—	`ω₀.eq_1` `k_pos` `m_pos`

---

← Back to Index