theorem
proved
hyperbolic_ode_unique
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.DAlembert.AnalyticBridge on GitHub at line 352.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
G -
G -
Energy -
G -
ode_zero_uniqueness -
via -
SatisfiesHyperbolicODE -
of -
is -
of -
is -
E -
of -
is -
G -
of -
is -
Cost -
sub -
pow -
sub -
constant
used by
formal source
349 5. E'(t) = 2 f'(t) f''(t) - 2 f(t) f'(t) = 2 f'(t) f(t) - 2 f(t) f'(t) = 0.
350 6. Since E(0) = 0, E(t) = 0 for all t, so f'(t)² = f(t)².
351 7. This implies f(t) = 0 for all t. -/
352theorem hyperbolic_ode_unique :
353 ∀ G : ℝ → ℝ,
354 SatisfiesHyperbolicODE G →
355 G 0 = 0 →
356 deriv G 0 = 0 →
357 ContDiff ℝ 2 G →
358 ∀ t, G t = Real.cosh t - 1 := by
359 intro G hODE hG0 hGderiv0 hSmooth t
360 let y := fun x => G x + 1
361 let f := fun x => y x - Real.cosh x
362 -- We want to show f x = 0
363 have hf0 : f 0 = 0 := by simp [f, y, hG0]
364 have hfd0 : deriv f 0 = 0 := by
365 unfold f y
366 rw [deriv_sub, deriv_add_const, hGderiv0, Real.deriv_cosh, Real.sinh_zero, sub_zero]
367 · exact hSmooth.differentiable (by decide) |>.differentiableAt
368 · exact Real.differentiable_cosh 0 |>.differentiableAt
369 have hf_ode : ∀ x, deriv (deriv f) x = f x := by
370 intro x
371 unfold f y
372 rw [deriv_sub, deriv_add_const, Real.deriv_cosh]
373 rw [deriv_sub, deriv_add_const, Real.deriv_sinh, hODE]
374 · ring
375 · exact hSmooth.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt
376 · exact Real.differentiable_sinh x |>.differentiableAt
377 · exact hSmooth.differentiable (by decide) |>.differentiableAt
378 · exact Real.differentiable_cosh x |>.differentiableAt
379 -- Differentiability of f
380 have hf_diff : Differentiable ℝ f := by
381 apply (hSmooth.add contDiff_const).sub Real.contDiff_cosh |>.differentiable (by decide)
382