H_dAlembert_of_composition

formal source

  71    h'.add (continuous_const : Continuous fun _ : ℝ => (1 : ℝ))
  72  simpa [H, G] using h_add
  73
  74private theorem H_dAlembert_of_composition (F : ℝ → ℝ)
  75    (hComp : SatisfiesCompositionLaw F) :
  76    ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u := by
  77  let Gf : ℝ → ℝ := G F
  78  have h_direct : DirectCoshAdd Gf :=
  79    CoshAddIdentity_implies_DirectCoshAdd F ((composition_law_equiv_coshAdd F).mp hComp)
  80  intro t u
  81  have hG := h_direct t u
  82  have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
  83    calc
  84      (Gf (t + u) + 1) + (Gf (t - u) + 1)
  85          = (Gf (t + u) + Gf (t - u)) + 2 := by ring
  86      _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by
  87            simpa [Gf] using hG
  88      _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
  89  simpa [Gf, H, G] using h_goal
  90
  91/-- Official public T5 theorem with an explicit Aczél kernel seam.
  92
  93The public statement now takes the primitive cost hypotheses directly and uses
  94`AczelRegularityKernel` as the sole regularity bridge. This makes the T5 seam
  95explicit without routing through `JensenSketch`. -/
  96theorem primitive_to_uniqueness_of_kernel (F : ℝ → ℝ)
  97    (hF : PrimitiveCostHypotheses F)
  98    (hKernel : AczelRegularityKernel (H F)) :
  99    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 100  have h_H0 : H F 0 = 1 := H_one_of_normalized F hF.normalized
 101  have h_H_cont : Continuous (H F) :=
 102    H_continuous_of_positive_continuous F hF.continuous
 103  have h_H_dAlembert : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u :=
 104    H_dAlembert_of_composition F hF.composition