representation_formula

proof body

Tactic-mode proof.

  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]
  95    have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
  96    have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
  97    linarith [hF_const d 0]
  98  -- Step 2: ∫₀ᵈ H(t-u) du = Phi(t) - Phi(t-d)
  99  have h_refl : ∀ d, ∫ u in (0:ℝ)..d, H (t - u) = Phi H t - Phi H (t - d) := by
 100    intro d
 101    let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t - u)) - (Phi H t - Phi H (t - d))
 102    suffices hF : F d = 0 by simp only [F] at hF; linarith
 103    have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
 104      intro d
 105      have h1 := intervalIntegral.integral_hasDerivAt_right
 106        (h_cont_sub.intervalIntegrable 0 d)
 107        h_cont_sub.aestronglyMeasurable.stronglyMeasurableAtFilter
 108        h_cont_sub.continuousAt
 109      have h_neg_raw := (hasDerivAt_id d).const_sub t
 110      have h_neg : HasDerivAt (fun d => t - d) (-1) d := by simpa using h_neg_raw
 111      have h_comp := (phi_hasDerivAt H h_cont (t - d)).comp d h_neg
 112      have h2 : HasDerivAt (fun d => Phi H t - Phi H (t - d)) (H (t - d)) d := by
 113        have h_phi_td : HasDerivAt (fun d => Phi H (t - d)) (H (t - d) * (-1)) d := by
 114          simpa only [Function.comp_def] using h_comp
 115        convert (hasDerivAt_const d (Phi H t)).sub h_phi_td using 1; ring
 116      show HasDerivAt F 0 d
 117      have h3 : HasDerivAt F (H (t - d) - H (t - d)) d := h1.sub h2
 118      simpa using h3
 119    have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero, sub_zero]
 120    have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
 121    have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
 122    linarith [hF_const d 0]
 123  -- Step 3: Combine via d'Alembert
 124  have h_add_int : IntervalIntegrable (fun u => H (t + u)) volume 0 δ :=
 125    h_cont_add.intervalIntegrable 0 δ
 126  have h_sub_int : IntervalIntegrable (fun u => H (t - u)) volume 0 δ :=
 127    h_cont_sub.intervalIntegrable 0 δ
 128  have h_integral : Phi H (t + δ) - Phi H (t - δ) = 2 * H t * Phi H δ := by
 129    have h1 := h_shift δ
 130    have h2 := h_refl δ
 131    have h3 : (∫ u in (0:ℝ)..δ, H (t + u)) + (∫ u in (0:ℝ)..δ, H (t - u)) =
 132        2 * H t * Phi H δ := by
 133      rw [← intervalIntegral.integral_add h_add_int h_sub_int]
 134      simp_rw [show ∀ u, H (t + u) + H (t - u) = 2 * H t * H u from h_dAl t]
 135      exact intervalIntegral.integral_const_mul (2 * H t) H
 136    linarith
 137  field_simp at h_integral ⊢; linarith
 138