`BookProof.DampedOscillatorEnergy.criticallyDamped_energy` (t : ℝ) : dampedEnergy 1 (fun s => Real.exp (-s)) (fun s => -Real.exp (-s)) t = Real.exp (-t) ^ 2

Initializing...

`BookProof.DampedOscillatorEnergy.criticallyDamped_energy` (t : ℝ) : dampedEnergy 1 (fun s => Real.exp (-s)) (fun s => -Real.exp (-s)) t = Real.exp (-t) ^ 2 · Prove2Me