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
proof body
Tactic-mode proof.
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`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.