phi_differentiable

formal source

  38  intervalIntegral.integral_hasDerivAt_right (h_cont.intervalIntegrable 0 t)
  39    h_cont.aestronglyMeasurable.stronglyMeasurableAtFilter h_cont.continuousAt
  40
  41private lemma phi_differentiable (H : ℝ → ℝ) (h_cont : Continuous H) :
  42    Differentiable ℝ (Phi H) :=
  43  fun t => (phi_hasDerivAt H h_cont t).differentiableAt
  44
  45private lemma deriv_phi_eq (H : ℝ → ℝ) (h_cont : Continuous H) : deriv (Phi H) = H :=
  46  funext fun t => (phi_hasDerivAt H h_cont t).deriv
  47
  48private lemma exists_integral_ne_zero (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) :
  49    ∃ δ : ℝ, 0 < δ ∧ Phi H δ ≠ 0 := by
  50  have h_pos : (0 : ℝ) < H 0 := by rw [h_one]; exact one_pos
  51  have h_ev : ∀ᶠ x in nhds (0 : ℝ), (0 : ℝ) < H x :=
  52    h_cont.continuousAt.eventually (Ioi_mem_nhds h_pos)
  53  obtain ⟨ε, hε_pos, hε⟩ := Metric.eventually_nhds_iff.mp h_ev
  54  refine ⟨ε / 2, by positivity, ?_⟩
  55  intro h_eq
  56  have hδ_pos : (0 : ℝ) < ε / 2 := by positivity
  57  obtain ⟨c, hc_mem, hc_eq⟩ := exists_hasDerivAt_eq_slope (Phi H) H hδ_pos
  58    ((phi_differentiable H h_cont).continuous.continuousOn)
  59    (fun x _ => phi_hasDerivAt H h_cont x)
  60  rw [phi_zero, h_eq, sub_zero, zero_div] at hc_eq
  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.