`smooth`

definition

show as: view math explainer →

module: IndisputableMonolith.Cost.AczelProof
domain: Cost
line: 27 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.AczelProof on GitHub at line 27.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  24
  25noncomputable section
  26
  27private abbrev smooth : WithTop ℕ∞ := (⊤ : ℕ∞)
  28
  29/-! ## Phase 1: Integration Bootstrap (Continuous → C^∞) -/
  30
  31private def Phi (H : ℝ → ℝ) (t : ℝ) : ℝ := ∫ s in (0 : ℝ)..t, H s
  32
  33private lemma phi_zero (H : ℝ → ℝ) : Phi H 0 = 0 := by
  34  simp [Phi, intervalIntegral.integral_same]
  35
  36private lemma phi_hasDerivAt (H : ℝ → ℝ) (h_cont : Continuous H) (t : ℝ) :
  37    HasDerivAt (Phi H) (H t) t :=
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.