representation_formula

formal source

  61  linarith [hε (show dist c 0 < ε by
  62    simp only [Real.dist_eq, sub_zero, abs_of_pos hc_mem.1]; linarith [hc_mem.2])]
  63
  64private lemma representation_formula (H : ℝ → ℝ) (h_cont : Continuous H)
  65    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
  66    {δ : ℝ} (hδ_ne : Phi H δ ≠ 0) (t : ℝ) :
  67    H t = (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ) := by
  68  -- Strategy: avoid integral substitution by using FTC + is_const_of_deriv_eq_zero.
  69  -- We prove ∫₀ᵈ H(t+u)du = Phi(t+d)-Phi(t) and ∫₀ᵈ H(t-u)du = Phi(t)-Phi(t-d)
  70  -- by showing both sides have the same derivative (w.r.t. d) and agree at d=0.
  71  -- Then the d'Alembert equation integrated gives the representation.
  72  have h_cont_add : Continuous (fun u => H (t + u)) :=
  73    h_cont.comp (continuous_const.add continuous_id)
  74  have h_cont_sub : Continuous (fun u => H (t - u)) :=
  75    h_cont.comp (continuous_const.sub continuous_id)
  76  -- Step 1: ∫₀ᵈ H(t+u) du = Phi(t+d) - Phi(t)
  77  -- Proof: define F(d) = LHS - RHS, show F'=0 and F(0)=0, so F=0.
  78  have h_shift : ∀ d, ∫ u in (0:ℝ)..d, H (t + u) = Phi H (t + d) - Phi H t := by
  79    intro d
  80    let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t + u)) - (Phi H (t + d) - Phi H t)
  81    suffices hF : F d = 0 by simp only [F] at hF; linarith
  82    have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
  83      intro d
  84      have h1 := intervalIntegral.integral_hasDerivAt_right
  85        (h_cont_add.intervalIntegrable 0 d)
  86        h_cont_add.aestronglyMeasurable.stronglyMeasurableAtFilter
  87        h_cont_add.continuousAt
  88      have h2_raw := (phi_hasDerivAt H h_cont (t + d)).comp d ((hasDerivAt_id d).const_add t)
  89      have h2 : HasDerivAt (fun d => Phi H (t + d)) (H (t + d)) d := by
  90        simpa only [mul_one, Function.comp_def] using h2_raw
  91      show HasDerivAt F 0 d
  92      have h3 : HasDerivAt F (H (t + d) - H (t + d)) d := h1.sub (h2.sub_const _)
  93      simpa using h3
  94    have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero]