def
definition
ZeroDefectImpliesCoshHypothesis
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.DAlembert.Stability on GitHub at line 342.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
339/-! ## Zero Defect Implies Exact Solution -/
340
341/-- When the defect is exactly zero, H is an exact cosh solution. -/
342def ZeroDefectImpliesCoshHypothesis
343 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) : Prop :=
344 UniformDefectBound H T 0 →
345 ∀ t : ℝ, |t| ≤ T → H t = Real.cosh (Real.sqrt hyp.curvature * t)
346
347theorem zero_defect_implies_cosh
348 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
349 (h_zero : UniformDefectBound H T 0)
350 (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
351 ∀ t : ℝ, |t| ≤ T → H t = Real.cosh (Real.sqrt hyp.curvature * t) := by
352 exact h_zero_hyp h_zero
353
354/-- Zero defect + calibration a = 1 gives H = cosh exactly. -/
355theorem zero_defect_calibrated_implies_cosh
356 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
357 (h_a1 : hyp.curvature = 1)
358 (h_zero : UniformDefectBound H T 0)
359 (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
360 ∀ t : ℝ, |t| ≤ T → H t = Real.cosh t := by
361 intro t ht
362 have h := zero_defect_implies_cosh H T hyp h_zero h_zero_hyp t ht
363 simp only [h_a1, Real.sqrt_one, one_mul] at h
364 exact h
365
366end Stability
367end DAlembert
368end Foundation
369end IndisputableMonolith