aczel_classification_conditional

formal source

 117    ∃ lam : ℝ, ∀ t, f t = Real.exp (lam * t)
 118
 119/-- The full Aczél classification, conditional on the two bridge lemmas. -/
 120theorem aczel_classification_conditional
 121    (H : ℝ → ℝ)
 122    (h_one : H 0 = 1)
 123    (h_cont : Continuous H)
 124    (h_dA : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
 125    (h_phi_mult : H_PhiMultiplicative H)
 126    (h_cauchy : H_CauchyToExponential)
 127    (h_ge_one : ∀ t, 1 ≤ H t) :
 128    ∃ lam : ℝ, ∀ t, H t = Real.cosh (lam * t) := by
 129  have h_phi_cont : Continuous (phi H) := by
 130    unfold phi
 131    exact h_cont.add ((h_cont.pow 2).sub continuous_const).sqrt
 132  have h_phi_pos : ∀ t, 0 < phi H t := fun t => phi_pos H t (h_ge_one t)
 133  have h_phi_zero : phi H 0 = 1 := phi_at_zero H h_one
 134  have h_phi_cauchy : ∀ t u, phi H (t + u) = phi H t * phi H u :=
 135    fun t u => h_phi_mult t u (h_ge_one t) (h_ge_one u)
 136  obtain ⟨lam_, hlam⟩ := h_cauchy (phi H) h_phi_cont h_phi_pos h_phi_zero h_phi_cauchy
 137  refine ⟨lam_, fun t => ?_⟩
 138  have h_phi_exp : phi H t = Real.exp (lam_ * t) := hlam t
 139  have h_phi_neg : phi H (-t) = Real.exp (-(lam_ * t)) := by
 140    rw [hlam (-t)]; ring_nf
 141  have h_H_from_phi := H_from_phi H t (h_ge_one t)
 142  rw [h_phi_exp] at h_H_from_phi
 143  rw [Real.cosh_eq]
 144  convert h_H_from_phi using 1
 145  rw [exp_neg]
 146
 147end
 148
 149end IndisputableMonolith.Cost.CauchyAuxiliary