washburn_uniqueness_aczel

proof body

Tactic-mode proof.

 182  intro x hx
 183  have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
 184  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
 185  let Gf : ℝ → ℝ := G F
 186  let Hf : ℝ → ℝ := H F
 187  have h_H0 : Hf 0 = 1 := by
 188    show H F 0 = 1
 189    simp only [H, G, Real.exp_zero]
 190    rw [hNorm]
 191    ring
 192  have h_G_cont : Continuous Gf := by
 193    have h := ContinuousOn.comp_continuous hCont continuous_exp
 194    have h' : Continuous (fun t => F (Real.exp t)) :=
 195      h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
 196    simpa [Gf, G] using h'
 197  have h_H_cont : Continuous Hf := by
 198    simpa [Hf, H] using h_G_cont.add continuous_const
 199  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 200  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 201    intro t u
 202    have hG := h_direct t u
 203    have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
 204      calc
 205        (Gf (t + u) + 1) + (Gf (t - u) + 1)
 206            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
 207        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simpa [hG]
 208        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
 209    simpa [Hf, H, Gf] using h_goal
 210  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
 211    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
 212      simpa [Gf, G] using hCalib
 213    have hderiv : deriv Hf = deriv Gf := by
 214      funext t
 215      change deriv (fun y => Gf y + 1) t = deriv Gf t
 216      simpa using (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
 217    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
 218    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
 219  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
 220    dAlembert_cosh_solution_aczel Hf h_H0 h_H_cont h_dAlembert h_H_d2
 221  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := fun t => by
 222    have : Gf t + 1 = Real.cosh t := h_H_cosh t
 223    linarith
 224  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
 225  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
 226    Jcost_G_eq_cosh_sub_one (Real.log x)
 227  calc
 228    F x = F (Real.exp (Real.log x)) := by rw [ht]
 229    _ = Gf (Real.log x) := rfl
 230    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
 231    _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
 232    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
 233    _ = Cost.Jcost x := by simpa [ht]
 234
 235end FunctionalEquation
 236end Cost
 237end IndisputableMonolith