washburn_uniqueness_of_contDiff

proof body

Tactic-mode proof.

 196  intro x hx
 197  let Gf : ℝ → ℝ := G F
 198  let Hf : ℝ → ℝ := H F
 199  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
 200  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 201  have h_H0 : Hf 0 = 1 := by
 202    dsimp [Hf]
 203    simpa [H, G, IsNormalized] using hNorm
 204  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 205    intro t u
 206    have hG := h_direct t u
 207    have h_goal :
 208        (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
 209      calc
 210        (Gf (t + u) + 1) + (Gf (t - u) + 1)
 211            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
 212        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
 213        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
 214    simpa [Hf, H, Gf] using h_goal
 215  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
 216    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
 217      simpa [Gf, G, IsCalibrated] using hCalib
 218    have hderiv : deriv Hf = deriv Gf := by
 219      funext t
 220      change deriv (fun y => Gf y + 1) t = deriv Gf t
 221      exact deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ))
 222    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
 223    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
 224  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
 225    dAlembert_cosh_solution_of_contDiff Hf h_H0 h_dAlembert (by simpa [Hf] using h_diff) h_H_d2
 226  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
 227    intro t
 228    have hH := h_H_cosh t
 229    have hH' : Gf t + 1 = Real.cosh t := by
 230      simpa [Hf, H, Gf] using hH
 231    linarith
 232  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
 233  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
 234    Jcost_G_eq_cosh_sub_one (Real.log x)
 235  calc
 236    F x = F (Real.exp (Real.log x)) := by rw [ht]
 237    _ = Gf (Real.log x) := rfl
 238    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
 239    _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
 240    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
 241    _ = Cost.Jcost x := by rw [ht]
 242
 243end
 244
 245end FunctionalEquation
 246end Cost
 247end IndisputableMonolith