H_AczelClassification

formal source

  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
  98  simp [Phi, intervalIntegral.integral_same]
  99
 100private lemma phi_hasDerivAt (H : ℝ → ℝ) (h_cont : Continuous H) (t : ℝ) :
 101    HasDerivAt (Phi H) (H t) t :=
 102  intervalIntegral.integral_hasDerivAt_right (h_cont.intervalIntegrable 0 t)
 103    h_cont.aestronglyMeasurable.stronglyMeasurableAtFilter h_cont.continuousAt
 104
 105private lemma phi_differentiable (H : ℝ → ℝ) (h_cont : Continuous H) :
 106    Differentiable ℝ (Phi H) :=
 107  fun t => (phi_hasDerivAt H h_cont t).differentiableAt
 108
 109private lemma deriv_phi_eq (H : ℝ → ℝ) (h_cont : Continuous H) : deriv (Phi H) = H :=
 110  funext fun t => (phi_hasDerivAt H h_cont t).deriv
 111
 112private lemma exists_integral_ne_zero (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) :