exists_integral_ne_zero

formal source

 109private lemma deriv_phi_eq (H : ℝ → ℝ) (h_cont : Continuous H) : deriv (Phi H) = H :=
 110  funext fun t => (phi_hasDerivAt H h_cont t).deriv
 111
 112private lemma exists_integral_ne_zero (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) :
 113    ∃ δ : ℝ, 0 < δ ∧ Phi H δ ≠ 0 := by
 114  have h_pos : (0 : ℝ) < H 0 := by rw [h_one]; exact one_pos
 115  have h_ev : ∀ᶠ x in nhds (0 : ℝ), (0 : ℝ) < H x :=
 116    h_cont.continuousAt.eventually (Ioi_mem_nhds h_pos)
 117  obtain ⟨ε, hε_pos, hε⟩ := Metric.eventually_nhds_iff.mp h_ev
 118  refine ⟨ε / 2, by positivity, ?_⟩
 119  intro h_eq
 120  have hδ_pos : (0 : ℝ) < ε / 2 := by positivity
 121  obtain ⟨c, hc_mem, hc_eq⟩ := exists_hasDerivAt_eq_slope (Phi H) H hδ_pos
 122    ((phi_differentiable H h_cont).continuous.continuousOn)
 123    (fun x _ => phi_hasDerivAt H h_cont x)
 124  rw [phi_zero, h_eq, sub_zero, zero_div] at hc_eq
 125  linarith [hε (show dist c 0 < ε by
 126    simp only [Real.dist_eq, sub_zero, abs_of_pos hc_mem.1]; linarith [hc_mem.2])]
 127
 128/-- The representation formula: H(t) = (Φ(t+δ) − Φ(t−δ)) / (2·Φ(δ)).
 129    This is the key identity that bootstraps regularity. -/
 130private lemma representation_formula (H : ℝ → ℝ) (h_cont : Continuous H)
 131    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
 132    {δ : ℝ} (hδ_ne : Phi H δ ≠ 0) (t : ℝ) :
 133    H t = (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ) := by
 134  have h_cont_add : Continuous (fun u => H (t + u)) :=
 135    h_cont.comp (continuous_const.add continuous_id)
 136  have h_cont_sub : Continuous (fun u => H (t - u)) :=
 137    h_cont.comp (continuous_const.sub continuous_id)
 138  have h_shift : ∀ d, ∫ u in (0:ℝ)..d, H (t + u) = Phi H (t + d) - Phi H t := by
 139    intro d
 140    let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t + u)) - (Phi H (t + d) - Phi H t)
 141    suffices hF : F d = 0 by simp only [F] at hF; linarith
 142    have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by