dAlembert_double_angle

formal source

  64    apply hx (Set.mem_Icc.mpr ⟨by linarith [abs_le.mp ht], by linarith [abs_le.mp ht]⟩)⟩
  65
  66/-- H3: d'Alembert + H(0)=1 implies H(2t) = 2H(t)² − 1. -/
  67theorem dAlembert_double_angle (H : ℝ → ℝ)
  68    (h_one : H 0 = 1)
  69    (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
  70    ∀ t, H (2 * t) = 2 * H t ^ 2 - 1 := by
  71  intro t
  72  have h := h_dAlembert t t
  73  have : t + t = 2 * t := by ring
  74  rw [this] at h
  75  have : t - t = 0 := by ring
  76  rw [this, h_one] at h
  77  nlinarith [sq (H t)]
  78
  79/-! ## §2 The Classification Prop (kept for backward compatibility) -/
  80
  81/-- The Aczél classification statement. Now a PROVED theorem, no longer a hypothesis. -/
  82def H_AczelClassification : Prop :=
  83  ∀ (H : ℝ → ℝ),
  84    H 0 = 1 →
  85    Continuous H →
  86    (∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) →
  87    ContDiff ℝ ⊤ H
  88
  89/-! ## §3 Integration Bootstrap: Continuous → C^∞ -/
  90
  91noncomputable section
  92
  93private abbrev smooth : WithTop ℕ∞ := (⊤ : ℕ∞)
  94
  95private def Phi (H : ℝ → ℝ) (t : ℝ) : ℝ := ∫ s in (0 : ℝ)..t, H s
  96
  97private lemma phi_zero (H : ℝ → ℝ) : Phi H 0 = 0 := by