Аналіз I, Розділ 11.5: Ріманова інтегровність неперервних функцій

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Ріманова інтегровність рівномірно неперервних функцій.
• Ріманова інтегровність обмежених неперервних функцій.

theorem Chapter11.integ_of_uniform_cts {I : BoundedInterval} {f : ℝ → ℝ} (hf : UniformContinuousOn f ↑I) : IntegrableOn f I

Теорема 11.5.1

theorem Chapter11.integ_of_cts {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f ↑(BoundedInterval.Icc a b)) : IntegrableOn f (BoundedInterval.Icc a b)

Наслідок 11.5.2

theorem Chapter11.integ_of_bdd_cts {I : BoundedInterval} {f : ℝ → ℝ} (hbound : Chapter9.BddOn f ↑I) (hf : ContinuousOn f ↑I) : IntegrableOn f I

Твердження 11.5.3

@[reducible, inline]

abbrev Chapter11.PiecewiseContinuousOn (f : ℝ → ℝ) (I : BoundedInterval) : Prop

Визначення 11.5.4

Equations

• Chapter11.PiecewiseContinuousOn f I = ∃ (P : Chapter11.Partition I), ∀ J ∈ P.intervals, ContinuousOn f ↑J

@[reducible, inline]

noncomputable abbrev Chapter11.f_11_5_5 : ℝ → ℝ

Приклад 11.5.5

Equations

• Chapter11.f_11_5_5 x = if x < 2 then x ^ 2 else if x = 2 then 7 else x ^ 3

theorem Chapter11.integ_of_bdd_piecewise_cts {I : BoundedInterval} {f : ℝ → ℝ} (hbound : Chapter9.BddOn f ↑I) (hf : PiecewiseContinuousOn f I) : IntegrableOn f I

Твердження 11.5.6 / Вправа 11.5.1

theorem Chapter11.integ_zero {a b : ℝ} (hab : a ≤ b) (f : ℝ → ℝ) (hf : ContinuousOn f ↑(BoundedInterval.Icc a b)) (hnonneg : MajorizesOn f (fun (x : ℝ) => 0) (BoundedInterval.Icc a b)) (hinteg : integ f (BoundedInterval.Icc a b) = 0) (x : ℝ) : x ∈ BoundedInterval.Icc a b → f x = 0

Вправа 11.5.2