IndisputableMonolith.Foundation.DAlembert.Stability

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.FunctionalEquation
   4
   5/-!
   6# D'Alembert Stability Theory
   7
   8This module formalizes the stability estimates for near-solutions of the
   9d'Alembert functional equation, following the development in:
  10
  11  J. Washburn & M. Zlatanović, "Uniqueness of the Canonical Reciprocal Cost"
  12
  13## Main Results
  14
  151. **d'Alembert Defect** (Definition 7.1): Measures deviation from the d'Alembert identity
  162. **Stability Theorem** (Theorem 7.1): Quantitative bounds when defect is small
  173. **Cost Stability Corollary** (Corollary 7.1): Transfer to the cost functional F
  18
  19## Mathematical Content
  20
  21The d'Alembert functional equation is:
  22  H(t+u) + H(t-u) = 2·H(t)·H(u)
  23
  24The defect measures the failure of this identity:
  25  Δ_H(t,u) := H(t+u) + H(t-u) - 2·H(t)·H(u)
  26
  27The stability theorem shows that if:
  28- H is C³ and even with H(0) = 1
  29- The defect is bounded by ε on [-T, T]²
  30- H''(0) = a > 0
  31
  32Then H is close to cosh(√a·t) with explicit error bounds.
  33
  34## References
  35
  36- Aczél, "Lectures on Functional Equations" (1966)
  37- Kuczma, "An Introduction to the Theory of Functional Equations" (2009)
  38-/
  39
  40namespace IndisputableMonolith
  41namespace Foundation
  42namespace DAlembert
  43namespace Stability
  44
  45open Real Cost.FunctionalEquation
  46
  47/-! ## Definition 7.1: The d'Alembert Defect -/
  48
  49/-- **Definition 7.1 (d'Alembert Defect)**
  50
  51The defect measures the deviation from the d'Alembert functional equation.
  52For H : ℝ → ℝ, the defect at (t, u) is:
  53  Δ_H(t,u) := H(t+u) + H(t-u) - 2·H(t)·H(u)
  54
  55When Δ_H ≡ 0, H is an exact d'Alembert solution.
  56When |Δ_H| ≤ ε, H is an approximate solution. -/
  57def dAlembertDefect (H : ℝ → ℝ) (t u : ℝ) : ℝ :=
  58  H (t + u) + H (t - u) - 2 * H t * H u
  59
  60/-- The defect is zero iff H satisfies the d'Alembert equation at (t, u). -/
  61lemma defect_zero_iff_dAlembert (H : ℝ → ℝ) (t u : ℝ) :
  62    dAlembertDefect H t u = 0 ↔ H (t + u) + H (t - u) = 2 * H t * H u := by
  63  simp [dAlembertDefect, sub_eq_zero]
  64
  65/-- For even H with H(0) = 1, the defect is symmetric in t ↔ -t. -/
  66lemma defect_even_in_t (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
  67    dAlembertDefect H t u = dAlembertDefect H (-t) u := by
  68  simp only [dAlembertDefect]
  69  -- By evenness: H(-x) = H x, so H x = H(-x) by symmetry
  70  have h1 : H (t + u) = H (-t - u) := by
  71    calc H (t + u) = H (-(- (t + u))) := by ring_nf
  72      _ = H (-(-t - u)) := by ring_nf
  73      _ = H (-t - u) := hEven _
  74  have h2 : H (t - u) = H (-t + u) := by
  75    calc H (t - u) = H (-(-(t - u))) := by ring_nf
  76      _ = H (-(-t + u)) := by ring_nf
  77      _ = H (-t + u) := hEven _
  78  have h3 : H t = H (-t) := (hEven t).symm
  79  rw [h1, h2, h3]
  80  ring
  81
  82/-- The defect is symmetric in u ↔ -u. -/
  83lemma defect_even_in_u (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
  84    dAlembertDefect H t u = dAlembertDefect H t (-u) := by
  85  simp only [dAlembertDefect]
  86  have h1 : H u = H (-u) := (hEven u).symm
  87  -- Goal: H(t+u) + H(t-u) - 2*H(t)*H(u) = H(t-(-u)) + H(t+(-u)) - 2*H(t)*H(-u)
  88  -- Note: t - (-u) = t + u, t + (-u) = t - u
  89  -- So RHS = H(t+u) + H(t-u) - 2*H(t)*H(-u)
  90  -- With h1: H(u) = H(-u), the equation becomes LHS = LHS
  91  have heq1 : t - (-u) = t + u := by ring
  92  have heq2 : t + (-u) = t - u := by ring
  93  rw [heq1, heq2, ← h1]
  94  ring
  95
  96/-- The defect is symmetric: Δ(t,u) = Δ(u,t) when H is even. -/
  97lemma defect_symmetric (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
  98    dAlembertDefect H t u = dAlembertDefect H u t := by
  99  simp only [dAlembertDefect]
 100  have h1 : t + u = u + t := add_comm t u
 101  have h2 : H (t - u) = H (u - t) := by
 102    calc H (t - u) = H (-(u - t)) := by ring_nf
 103      _ = H (u - t) := hEven _
 104  rw [h1, h2]
 105  ring
 106
 107/-! ## Defect Bounds and Regularity -/
 108
 109/-- Uniform bound on the defect over a symmetric interval. -/
 110def UniformDefectBound (H : ℝ → ℝ) (T ε : ℝ) : Prop :=
 111  ∀ t u : ℝ, |t| ≤ T → |u| ≤ T → |dAlembertDefect H t u| ≤ ε
 112
 113/-- The standard hypothesis bundle for the stability theorem. -/
 114structure StabilityHypotheses (H : ℝ → ℝ) (T : ℝ) where
 115  /-- H is at least C³ on [-T, T] -/
 116  smooth : ContDiff ℝ 3 H
 117  /-- H is even: H(-t) = H(t) -/
 118  even : Function.Even H
 119  /-- H(0) = 1 -/
 120  normalized : H 0 = 1
 121  /-- H''(0) = a > 0 -/
 122  curvature : ℝ
 123  curvature_pos : 0 < curvature
 124  curvature_eq : deriv (deriv H) 0 = curvature
 125  /-- T > 0 -/
 126  T_pos : 0 < T
 127
 128/-- Bound constants for the stability estimate. -/
 129structure StabilityBounds (H : ℝ → ℝ) (T : ℝ) where
 130  /-- Uniform defect bound: |Δ_H(t,u)| ≤ ε for |t|,|u| ≤ T -/
 131  ε : ℝ
 132  ε_nonneg : 0 ≤ ε
 133  defect_bound : UniformDefectBound H T ε
 134  /-- Uniform bound on |H|: |H(t)| ≤ B for |t| ≤ T -/
 135  B : ℝ
 136  B_pos : 0 < B
 137  H_bound : ∀ t : ℝ, |t| ≤ T → |H t| ≤ B
 138  /-- Uniform bound on |H'''|: |H'''(t)| ≤ K for |t| ≤ T -/
 139  K : ℝ
 140  K_nonneg : 0 ≤ K
 141  H'''_bound : ∀ t : ℝ, |t| ≤ T → |iteratedDeriv 3 H t| ≤ K
 142
 143/-! ## The δ(h) Error Function -/
 144
 145/-- The error bound function δ(h) from Theorem 7.1.
 146
 147For step size h > 0, the local error is controlled by:
 148  δ(h) := ε/h² + (1+B)·K·h/3
 149
 150where:
 151- ε is the defect bound
 152- B is the H-bound
 153- K is the H'''-bound -/
 154noncomputable def δ_error (ε B K h : ℝ) : ℝ :=
 155  ε / h^2 + (1 + B) * K * h / 3
 156
 157/-- δ(h) is positive when ε, K, h > 0 and B ≥ 0. -/
 158lemma δ_error_pos (ε B K h : ℝ) (hε : 0 < ε) (hB : 0 ≤ B) (hK : 0 ≤ K) (hh : 0 < h) :
 159    0 < δ_error ε B K h := by
 160  unfold δ_error
 161  have h1 : 0 < ε / h^2 := div_pos hε (pow_pos hh 2)
 162  have h2 : 0 ≤ (1 + B) * K * h / 3 := by positivity
 163  linarith
 164
 165/-- Optimal choice of h minimizes δ(h).
 166
 167Taking dδ/dh = 0 gives: -2ε/h³ + (1+B)K/3 = 0
 168Solving: h³ = 6ε/((1+B)K), so h = (6ε/((1+B)K))^{1/3}
 169
 170This gives δ(h_opt) ~ O(ε^{1/3}) -/
 171noncomputable def optimal_h (ε B K : ℝ) : ℝ :=
 172  (6 * ε / ((1 + B) * K)) ^ (1/3 : ℝ)
 173
 174/-! ## Theorem 7.1: Main Stability Estimate -/
 175
 176/-- **Theorem 7.1 (d'Alembert Stability)**
 177
 178Let H ∈ C³([-T,T]) be even with H(0) = 1, and set a := H''(0) > 0.
 179
 180Define:
 181- ε := sup_{|t|,|u| ≤ T} |Δ_H(t,u)|  (defect bound)
 182- B := sup_{|t| ≤ T} |H(t)|          (function bound)
 183- K := sup_{|t| ≤ T} |H'''(t)|       (third derivative bound)
 184- δ(h) := ε/h² + (1+B)·K·h/3        (error function)
 185
 186Then for every h with 0 < h ≤ T and every t with |t| ≤ T - h:
 187
 188  |H(t) - cosh(√a·t)| ≤ (δ(h)/a) · (cosh(√a·|t|) - 1)
 189
 190When a = 1 and δ(h) is small, this shows H ≈ cosh on compact intervals. -/
 191def StabilityEstimate (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=
 192  ∀ h : ℝ, 0 < h → h ≤ T →
 193  ∀ t : ℝ, |t| ≤ T - h →
 194  |H t - Real.cosh (Real.sqrt a * t)| ≤
 195    (δ_error bounds.ε bounds.B bounds.K h / a) * (Real.cosh (Real.sqrt a * |t|) - 1)
 196
 197/-- The ODE intermediate step: from the defect bound, we derive H'' - a·H is small.
 198
 199This is equation (7.3) in the paper:
 200  |H''(t) - a·H(t)| ≤ δ(h)  for |t| ≤ T - h -/
 201def ODEApproximation (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=
 202  ∀ h : ℝ, 0 < h → h ≤ T →
 203  ∀ t : ℝ, |t| ≤ T - h →
 204  |deriv (deriv H) t - a * H t| ≤ δ_error bounds.ε bounds.B bounds.K h
 205
 206/-- **Key Lemma**: Taylor expansion + defect bound implies ODE approximation.
 207
 208From the integral form of Taylor's theorem:
 209  H(t+h) + H(t-h) = 2H(t) + h²H''(t) + O(h³)
 210
 211Combined with the defect identity:
 212  H(t+h) + H(t-h) = 2H(t)H(h) + Δ(t,h)
 213
 214We get:
 215  h²H''(t) ≈ 2H(t)(H(h) - 1) + Δ(t,h)
 216
 217For small h, H(h) ≈ 1 + (a/2)h², so:
 218  h²H''(t) ≈ a·h²·H(t) + Δ(t,h) + O(h³)
 219
 220Dividing by h² gives the ODE approximation. -/
 221def ODEApproximationHypothesis
 222    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
 223  ODEApproximation H T hyp.curvature bounds
 224
 225theorem ode_approximation_from_defect
 226    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
 227    (h_ode : ODEApproximationHypothesis H T hyp bounds) :
 228    ODEApproximation H T hyp.curvature bounds := by
 229  exact h_ode
 230
 231/-- **Key Lemma**: ODE approximation + Gronwall implies stability estimate.
 232
 233If |H''(t) - a·H(t)| ≤ δ and H(0) = cosh(0) = 1, H'(0) = sinh(0) = 0,
 234then the variation-of-parameters formula gives:
 235
 236  H(t) - cosh(√a·t) = ∫₀ᵗ (1/√a)·sinh(√a·(t-s))·r(s) ds
 237
 238where r(s) = H''(s) - a·H(s) satisfies |r(s)| ≤ δ.
 239
 240Bounding the integral gives:
 241  |H(t) - cosh(√a·t)| ≤ (δ/a)·(cosh(√a·|t|) - 1) -/
 242def StabilityFromODEHypothesis
 243    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
 244  ODEApproximation H T hyp.curvature bounds → StabilityEstimate H T hyp.curvature bounds
 245
 246theorem stability_from_ode_approx
 247    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
 248    (h_ode : ODEApproximation H T hyp.curvature bounds)
 249    (h_stab : StabilityFromODEHypothesis H T hyp bounds) :
 250    StabilityEstimate H T hyp.curvature bounds := by
 251  exact h_stab h_ode
 252
 253/-- **Theorem 7.1 (Complete Statement)** -/
 254theorem dAlembert_stability
 255    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
 256    (h_ode : ODEApproximationHypothesis H T hyp bounds)
 257    (h_stab : StabilityFromODEHypothesis H T hyp bounds) :
 258    StabilityEstimate H T hyp.curvature bounds := by
 259  have h_ode' := ode_approximation_from_defect H T hyp bounds h_ode
 260  exact stability_from_ode_approx H T hyp bounds h_ode' h_stab
 261
 262/-! ## Corollary 7.1: Stability for the Cost Functional -/
 263
 264/-- **Corollary 7.1 (Cost Functional Stability)**
 265
 266Let F(x) := H(log x) - 1 on ℝ₊, where H satisfies the stability hypotheses.
 267
 268If a is close to 1 and δ(h) is small, then F is uniformly close to the
 269canonical cost J(x) = cosh(log x) - 1 on compact subintervals of (0, ∞).
 270
 271When a = 1, the estimate simplifies to:
 272  |F(x) - J(x)| ≤ δ(h) · J(|x|) -/
 273def CostStabilityEstimate (F : ℝ → ℝ) (T a : ℝ) (δ : ℝ) : Prop :=
 274  ∀ x : ℝ, Real.exp (-(T)) < x → x < Real.exp T →
 275  |F x - Cost.Jcost x| ≤ (δ / a) * (Real.cosh (Real.sqrt a * |Real.log x|) - 1)
 276
 277/-- Transfer stability from H to F via F(x) = H(log x) - 1. -/
 278def CostStabilityTransferHypothesis
 279    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
 280  StabilityEstimate H T hyp.curvature bounds →
 281    ∀ (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T),
 282      ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
 283        |H (Real.log x) - 1 - Cost.Jcost x| ≤
 284          (δ_error bounds.ε bounds.B bounds.K h / hyp.curvature) *
 285          (Real.cosh (Real.sqrt hyp.curvature * |Real.log x|) - 1)
 286
 287theorem cost_stability_transfer
 288    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
 289    (h_stab : StabilityEstimate H T hyp.curvature bounds)
 290    (h_transfer : CostStabilityTransferHypothesis H T hyp bounds)
 291    (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
 292    ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
 293    |H (Real.log x) - 1 - Cost.Jcost x| ≤
 294      (δ_error bounds.ε bounds.B bounds.K h / hyp.curvature) *
 295      (Real.cosh (Real.sqrt hyp.curvature * |Real.log x|) - 1) := by
 296  exact h_transfer h_stab h hh_pos hh_le
 297
 298/-! ## Special Case: a = 1 (Standard Calibration) -/
 299
 300/-- When a = 1 (standard RS calibration), the stability estimate simplifies. -/
 301theorem stability_calibrated
 302    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
 303    (h_a1 : hyp.curvature = 1)
 304    (bounds : StabilityBounds H T)
 305    (h_stab : StabilityEstimate H T hyp.curvature bounds)
 306    (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
 307    ∀ t : ℝ, |t| ≤ T - h →
 308    |H t - Real.cosh t| ≤ δ_error bounds.ε bounds.B bounds.K h * (Real.cosh |t| - 1) := by
 309  intro t ht
 310  have h_main := h_stab h hh_pos hh_le t ht
 311  simp only [h_a1, Real.sqrt_one, one_mul, div_one] at h_main
 312  exact h_main
 313
 314/-- When a = 1, the cost stability simplifies to |F(x) - J(x)| ≤ δ · J(x). -/
 315theorem cost_stability_calibrated
 316    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
 317    (h_a1 : hyp.curvature = 1)
 318    (bounds : StabilityBounds H T)
 319    (h_stab : StabilityEstimate H T hyp.curvature bounds)
 320    (h_transfer : CostStabilityTransferHypothesis H T hyp bounds)
 321    (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
 322    ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
 323    |H (Real.log x) - 1 - Cost.Jcost x| ≤
 324      δ_error bounds.ε bounds.B bounds.K h * Cost.Jcost x := by
 325  intro x hx_lo hx_hi
 326  have h_main := cost_stability_transfer H T hyp bounds h_stab h_transfer h hh_pos hh_le x hx_lo hx_hi
 327  simp only [h_a1, Real.sqrt_one, one_mul, div_one] at h_main
 328  -- Need to show cosh(|log x|) - 1 = J(x) when x > 0
 329  have hx_pos : 0 < x := by linarith [Real.exp_pos (-(T-h))]
 330  have hJ : Cost.Jcost x = Real.cosh (Real.log x) - 1 := by
 331    have h1 := Cost.Jcost_exp_cosh (Real.log x)
 332    simp only [Real.exp_log hx_pos] at h1
 333    exact h1
 334  have h_cosh : Real.cosh (Real.log x) - 1 = Cost.Jcost x := by
 335    symm
 336    exact hJ
 337  simpa [h_cosh] using h_main
 338
 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
 370