H_continuous_of_positive_continuous

formal source

  62  have h0 : F 1 = 0 := by simpa [IsNormalized] using hNorm
  63  simp [H, G, h0]
  64
  65private theorem H_continuous_of_positive_continuous (F : ℝ → ℝ)
  66    (hCont : ContinuousOn F (Set.Ioi 0)) : Continuous (H F) := by
  67  have h := ContinuousOn.comp_continuous hCont Real.continuous_exp
  68  have h' : Continuous (fun t => F (Real.exp t)) :=
  69    h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
  70  have h_add : Continuous (fun t : ℝ => F (Real.exp t) + (1 : ℝ)) :=
  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`. -/