T5_uniqueness_complete

formal source

  24    as explicit hypotheses in the theorems below. -/
  25
  26/-- Full T5 Uniqueness Theorem (with explicit functional-identity hypothesis) -/
  27theorem T5_uniqueness_complete (F : ℝ → ℝ)
  28  (hSymm : ∀ {x}, 0 < x → F x = F x⁻¹)
  29  (hUnit : F 1 = 0)
  30  (hConvex : StrictConvexOn ℝ (Set.Ioi 0) F)
  31  (hCalib : deriv (deriv (F ∘ exp)) 0 = 1)
  32  (hCont : ContinuousOn F (Ioi 0))
  33  (hCoshAdd : FunctionalEquation.CoshAddIdentity F)
  34  (h_smooth_hyp : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F))
  35  (h_ode_hyp : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F))
  36  (h_cont_hyp : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F))
  37  (h_diff_hyp : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F))
  38  (h_bootstrap_hyp : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)) :
  39  ∀ {x : ℝ}, 0 < x → F x = Jcost x := by
  40  intro x hx
  41  -- Reduce to log coordinates and invoke d'Alembert uniqueness
  42  let Gf : ℝ → ℝ := FunctionalEquation.G F
  43  have h_even : Function.Even Gf := FunctionalEquation.G_even_of_reciprocal_symmetry F hSymm
  44  have h_G0 : Gf 0 = 0 := FunctionalEquation.G_zero_of_unit F hUnit
  45
  46  -- Gf is continuous on ℝ (F is continuous on (0,∞), exp is continuous, composition is continuous)
  47  have h_G_cont : Continuous Gf := by
  48    have h := ContinuousOn.comp_continuous hCont continuous_exp
  49    have h' : Continuous (fun t => F (Real.exp t)) :=
  50      h (by intro t; exact mem_Ioi.mpr (Real.exp_pos t))
  51    simpa [FunctionalEquation.G] using h'
  52
  53  -- Convert CoshAddIdentity F to DirectCoshAdd Gf
  54  have h_direct : FunctionalEquation.DirectCoshAdd Gf :=
  55    FunctionalEquation.CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  56
  57  -- Apply d'Alembert uniqueness (via the shifted H := G + 1) to get Gf(t) = cosh(t) - 1.