Аналіз I, Розділ 11.8: Інтеграл Рімана–Стєльтьєса

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

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

• Визначення α-довжини.
• Кусочно постійний інтеграл Рімана–Стєльтьєса.
• Повний інтеграл Рімана–Стєльтьєса.

Технічні примітки:

• У Lean зручніше робити визначення, такі як α-довжина та інтеграл Рімана–Стєльтьєса, повністю визначеними, призначаючи «сміттеві» значення у випадках, коли визначення не призначене для застосування. Для визначення α-довжини його передбачається застосовувати в контекстах, де існують ліві та праві границі, а функція продовжується константами ліворуч і праворуч від своєї передбаченої області визначення; наприклад, якщо функція f визначена на Icc 0 1, то передбачається, що f x = f 1 для всіх x ≥ 1 і f x = f 0 для всіх x ≤ 0; зокрема, на правому кінці відрізка значення функції повинно збігатися з її правим границею, і аналогічно для лівого кінця, хоча ми цього не вимагаємо у нашому визначенні α-довжини. (Для функцій, визначених на відкритих проміжках, таке продовження не має значення.)
• Поняття α-довжини та кусочно постійного інтегралу Рімана–Стєльтьєса передбачено для випадків, де існують ліві та праві границі, наприклад, для монотонних або неперервних функцій, хоча технічно вони мають сенс і без цих припущень. Повний інтеграл Рімана–Стєльтьєса призначений для функцій обмеженої варіації, хоча ми переважно зосередимося на спеціальному випадку монотонно зростаючих функцій.

@[reducible, inline]

noncomputable abbrev Chapter11.right_lim (f : ℝ → ℝ) (x₀ : ℝ) : ℝ

Ліві та праві границі. Якщо границя не існує, призначається «сміттеве» значення.

Equations

• Chapter11.right_lim f x₀ = lim (Filter.map f (nhdsWithin x₀ (Set.Ioi x₀)))

@[reducible, inline]

noncomputable abbrev Chapter11.left_lim (f : ℝ → ℝ) (x₀ : ℝ) : ℝ

Equations

• Chapter11.left_lim f x₀ = lim (Filter.map f (nhdsWithin x₀ (Set.Iio x₀)))

theorem Chapter11.right_lim_def {f : ℝ → ℝ} {x₀ L : ℝ} (h : Chapter9.Convergesto (Set.Ioi x₀) f L x₀) : right_lim f x₀ = L

theorem Chapter11.left_lim_def {f : ℝ → ℝ} {x₀ L : ℝ} (h : Chapter9.Convergesto (Set.Iio x₀) f L x₀) : left_lim f x₀ = L

@[reducible, inline]

noncomputable abbrev Chapter11.jump (f : ℝ → ℝ) (x₀ : ℝ) : ℝ

Equations

• Chapter11.jump f x₀ = Chapter11.right_lim f x₀ - Chapter11.left_lim f x₀

theorem Chapter11.right_lim_of_continuous {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : ∃ ε > 0, Set.Ico x₀ (x₀ + ε) ⊆ X) (hf : ContinuousWithinAt f X x₀) : right_lim f x₀ = f x₀

Праві границі існують для неперервних функцій.

theorem Chapter11.left_lim_of_continuous {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : ∃ ε > 0, Set.Ioc (x₀ - ε) x₀ ⊆ X) (hf : ContinuousWithinAt f X x₀) : left_lim f x₀ = f x₀

Ліві границі існують для неперервних функцій

theorem Chapter11.jump_of_continuous {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : X ∈ nhds x₀) (hf : ContinuousWithinAt f X x₀) : jump f x₀ = 0

Для неперервних функцій стрибків немає.

theorem Chapter11.right_lim_of_monotone {f : ℝ → ℝ} (x₀ : ℝ) (hf : Monotone f) : Chapter9.Convergesto (Set.Ioi x₀) f (sInf (f '' Set.Ioi x₀)) x₀

Right limits exist for monotone functions

theorem Chapter11.right_lim_of_monotone' {f : ℝ → ℝ} (x₀ : ℝ) (hf : Monotone f) : right_lim f x₀ = sInf (f '' Set.Ioi x₀)

theorem Chapter11.left_lim_of_monotone {f : ℝ → ℝ} (x₀ : ℝ) (hf : Monotone f) : Chapter9.Convergesto (Set.Iio x₀) f (sSup (f '' Set.Iio x₀)) x₀

Ліві границі існують для монотонних функцій

theorem Chapter11.left_lim_of_monotone' {f : ℝ → ℝ} (x₀ : ℝ) (hf : Monotone f) : left_lim f x₀ = sSup (f '' Set.Iio x₀)

theorem Chapter11.jump_of_monotone {f : ℝ → ℝ} (x₀ : ℝ) (hf : Monotone f) : 0 ≤ jump f x₀

theorem Chapter11.right_lim_le_left_lim_of_monotone {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hf : Monotone f) : right_lim f a ≤ left_lim f b

@[reducible, inline]

noncomputable abbrev Chapter11.α_length (α : ℝ → ℝ) (I : BoundedInterval) : ℝ

Визначення 11.8.1

Equations

• α[Chapter11.BoundedInterval.Icc a b]ₗ = if a ≤ b then Chapter11.right_lim α b - Chapter11.left_lim α a else 0
• α[Chapter11.BoundedInterval.Ico a b]ₗ = if a ≤ b then Chapter11.left_lim α b - Chapter11.left_lim α a else 0
• α[Chapter11.BoundedInterval.Ioc a b]ₗ = if a ≤ b then Chapter11.right_lim α b - Chapter11.right_lim α a else 0
• α[Chapter11.BoundedInterval.Ioo a b]ₗ = if a < b then Chapter11.left_lim α b - Chapter11.right_lim α a else 0

def Chapter11.«term_[_]ₗ» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Chapter11.«term_[_]ₗ».«delab_app.Chapter11.α_length» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter11.α_length_of_empty (α : ℝ → ℝ) {I : BoundedInterval} (hI : ↑I = ∅) : α[I]ₗ = 0

@[simp]

theorem Chapter11.α_length_of_pt {α : ℝ → ℝ} (a : ℝ) : α[BoundedInterval.Icc a a]ₗ = jump α a

theorem Chapter11.α_length_of_cts {α : ℝ → ℝ} {I : BoundedInterval} {a b : ℝ} (haa : a < I.a) (hab : I.a ≤ I.b) (hbb : I.b < b) (hI : I ⊆ BoundedInterval.Ioo a b) (hα : ContinuousOn α ↑(BoundedInterval.Ioo a b)) : α[I]ₗ = α I.b - α I.a

@[simp]

theorem Chapter11.α_len_of_id (I : BoundedInterval) : (fun (x : ℝ) => x)[I]ₗ = I.length

Приклад 11.8.3

@[reducible, inline]

abbrev Chapter11.BoundedInterval.joins' (K I J : BoundedInterval) : Prop

Покращена версія BoundedInterval.joins, яка також контролює α-довжину.

Equations

• K.joins' I J = (K.joins I J ∧ ∀ (α : ℝ → ℝ), α[K]ₗ = α[I]ₗ + α[J]ₗ)

theorem Chapter11.BoundedInterval.join_Icc_Ioc' {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Icc a c).joins' (Icc a b) (Ioc b c)

theorem Chapter11.BoundedInterval.join_Icc_Ioo' {a b c : ℝ} (hab : a ≤ b) (hbc : b < c) : (Ico a c).joins' (Icc a b) (Ioo b c)

theorem Chapter11.BoundedInterval.join_Ioc_Ioc' {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Ioc a c).joins' (Ioc a b) (Ioc b c)

theorem Chapter11.BoundedInterval.join_Ioc_Ioo' {a b c : ℝ} (hab : a ≤ b) (hbc : b < c) : (Ioo a c).joins' (Ioc a b) (Ioo b c)

theorem Chapter11.BoundedInterval.join_Ico_Icc' {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Icc a c).joins' (Ico a b) (Icc b c)

theorem Chapter11.BoundedInterval.join_Ico_Ico' {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Ico a c).joins' (Ico a b) (Ico b c)

theorem Chapter11.BoundedInterval.join_Ioo_Icc' {a b c : ℝ} (hab : a < b) (hbc : b ≤ c) : (Ioc a c).joins' (Ioo a b) (Icc b c)

theorem Chapter11.BoundedInterval.join_Ioo_Ico' {a b c : ℝ} (hab : a < b) (hbc : b ≤ c) : (Ioo a c).joins' (Ioo a b) (Ico b c)

theorem Chapter11.Partition.sum_of_α_length {I : BoundedInterval} (P : Partition I) (α : ℝ → ℝ) : ∑ J ∈ P.intervals, α[J]ₗ = α[I]ₗ

Теорема 11.8.4 / Вправа 11.8.1

@[reducible, inline]

noncomputable abbrev Chapter11.PiecewiseConstantWith.RS_integ (f : ℝ → ℝ) {I : BoundedInterval} (P : Partition I) (α : ℝ → ℝ) : ℝ

Визначення 11.8.5 (Кусочно постійний інтеграл Рімана–Стєльтьєса)

Equations

• Chapter11.PiecewiseConstantWith.RS_integ f P α = ∑ J ∈ P.intervals, Chapter11.constant_value_on f ↑J * α[J]ₗ

@[reducible, inline]

noncomputable abbrev Chapter11.f_11_8_6 (x : ℝ) : ℝ

Приклад 11.8.6

Equations

• Chapter11.f_11_8_6 x = if x < 2 then 4 else 2

@[reducible, inline]

noncomputable abbrev Chapter11.P_11_8_6 : Partition (BoundedInterval.Icc 1 3)

Equations

• Chapter11.P_11_8_6 = ⊥.join ⊥ Chapter11.P_11_8_6._proof_2

theorem Chapter11.f_11_8_6_RS_integ : (PiecewiseConstantWith.RS_integ f_11_8_6 P_11_8_6 fun (x : ℝ) => x) = 22

theorem Chapter11.PiecewiseConstantWith.RS_integ_eq_integ {f : ℝ → ℝ} {I : BoundedInterval} (P : Partition I) : (RS_integ f P fun (x : ℝ) => x) = integ f P

Приклад 11.8.7

theorem Chapter11.PiecewiseConstantWith.RS_integ_eq {f : ℝ → ℝ} {I : BoundedInterval} {P P' : Partition I} (hP : PiecewiseConstantWith f P) (hP' : PiecewiseConstantWith f P') (α : ℝ → ℝ) : RS_integ f P α = RS_integ f P' α

Аналог Твердження 11.2.13

@[reducible, inline]

noncomputable abbrev Chapter11.PiecewiseConstantOn.RS_integ (f : ℝ → ℝ) (I : BoundedInterval) (α : ℝ → ℝ) : ℝ

Equations

• Chapter11.PiecewiseConstantOn.RS_integ f I α = if h : Chapter11.PiecewiseConstantOn f I then Chapter11.PiecewiseConstantWith.RS_integ f (Exists.choose h) α else 0

theorem Chapter11.PiecewiseConstantOn.RS_integ_def {f : ℝ → ℝ} {I : BoundedInterval} {P : Partition I} (h : PiecewiseConstantWith f P) (α : ℝ → ℝ) : RS_integ f I α = PiecewiseConstantWith.RS_integ f P α

theorem Chapter11.α_length_nonneg_of_monotone {α : ℝ → ℝ} (hα : Monotone α) (I : BoundedInterval) : 0 ≤ α[I]ₗ

α-довжина невід’ємна, якщо α монотонна

theorem Chapter11.PiecewiseConstantOn.RS_integ_add {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) {α : ℝ → ℝ} (hα : Monotone α) : RS_integ (f + g) I α = RS_integ f I α + RS_integ g I α

Аналог теореми 11.2.16 (a) (Закони інтегрування) / Вправа 11.8.3

theorem Chapter11.PiecewiseConstantOn.RS_integ_smul {f : ℝ → ℝ} {I : BoundedInterval} (c : ℝ) (hf : PiecewiseConstantOn f I) {α : ℝ → ℝ} (hα : Monotone α) : RS_integ (c • f) I α = c * RS_integ f I α

Аналог теореми 11.2.16 (b) (Закони інтегрування) / Вправа 11.8.3

theorem Chapter11.PiecewiseConstantOn.RS_integ_sub {f g : ℝ → ℝ} {I : BoundedInterval} {α : ℝ → ℝ} (hα : Monotone α) (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : RS_integ (f - g) I α = RS_integ f I α - RS_integ g I α

Теорема 11.8.8 (c) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

theorem Chapter11.PiecewiseConstantOn.RS_integ_of_nonneg {f : ℝ → ℝ} {I : BoundedInterval} {α : ℝ → ℝ} (hα : Monotone α) (h : ∀ x ∈ I, 0 ≤ f x) (hf : PiecewiseConstantOn f I) : 0 ≤ RS_integ f I α

Теорема 11.8.8 (d) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

theorem Chapter11.PiecewiseConstantOn.RS_integ_mono {f g : ℝ → ℝ} {I : BoundedInterval} {α : ℝ → ℝ} (hα : Monotone α) (h : ∀ x ∈ I, f x ≤ g x) (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : RS_integ f I α ≤ RS_integ g I α

Теорема 11.8.8 (e) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

theorem Chapter11.PiecewiseConstantOn.RS_integ_const (c : ℝ) (I : BoundedInterval) {α : ℝ → ℝ} (hα : Monotone α) : RS_integ (fun (x : ℝ) => c) I α = c * α[I]ₗ

Теорема 11.8.8 (f) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

theorem Chapter11.PiecewiseConstantOn.RS_integ_const' {f : ℝ → ℝ} {I : BoundedInterval} {α : ℝ → ℝ} (hα : Monotone α) (h : ConstantOn f ↑I) : RS_integ f I α = constant_value_on f ↑I * α[I]ₗ

Теорема 11.8.8 (f) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

theorem Chapter11.PiecewiseConstantOn.RS_of_extend {I J : BoundedInterval} (hIJ : I ⊆ J) {f : ℝ → ℝ} (h : PiecewiseConstantOn f I) {α : ℝ → ℝ} (hα : Monotone α) : PiecewiseConstantOn (fun (x : ℝ) => if x ∈ I then f x else 0) J

Теорема 11.8.8 (g) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

theorem Chapter11.PiecewiseConstantOn.RS_integ_of_extend {I J : BoundedInterval} (hIJ : I ⊆ J) {f : ℝ → ℝ} (h : PiecewiseConstantOn f I) {α : ℝ → ℝ} (hα : Monotone α) : RS_integ (fun (x : ℝ) => if x ∈ I then f x else 0) J α = RS_integ f I α

Теорема 11.8.8 (g) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

theorem Chapter11.PiecewiseConstantOn.RS_integ_of_join {I J K : BoundedInterval} (hIJK : K.joins' I J) {f : ℝ → ℝ} (h : PiecewiseConstantOn f K) {α : ℝ → ℝ} (hα : Monotone α) : RS_integ f K α = RS_integ f I α + RS_integ f J α

Теорема 11.8.8 (h) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 11.8.8

@[reducible, inline]

noncomputable abbrev Chapter11.upper_RS_integral (f : ℝ → ℝ) (I : BoundedInterval) (α : ℝ → ℝ) : ℝ

Аналог визначення 11.3.2 (Верхній та нижній інтеграли Рімана )

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Chapter11.lower_RS_integral (f : ℝ → ℝ) (I : BoundedInterval) (α : ℝ → ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter11.RS_integral_bound_upper_of_bounded {f : ℝ → ℝ} {M : ℝ} {I : BoundedInterval} (h : ∀ x ∈ ↑I, |f x| ≤ M) {α : ℝ → ℝ} (hα : Monotone α) : M * α[I]ₗ ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I}

theorem Chapter11.RS_integral_bound_lower_of_bounded {f : ℝ → ℝ} {M : ℝ} {I : BoundedInterval} (h : ∀ x ∈ ↑I, |f x| ≤ M) {α : ℝ → ℝ} (hα : Monotone α) : -M * α[I]ₗ ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I}

theorem Chapter11.RS_integral_bound_upper_nonempty {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) : ((fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty

theorem Chapter11.RS_integral_bound_lower_nonempty {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) : ((fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty

theorem Chapter11.RS_integral_bound_lower_le_upper {f : ℝ → ℝ} {I : BoundedInterval} {a b : ℝ} {α : ℝ → ℝ} (hα : Monotone α) (ha : a ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) (hb : b ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) : b ≤ a

theorem Chapter11.RS_integral_bound_below {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) : BddBelow ((fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I})

theorem Chapter11.RS_integral_bound_above {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) : BddAbove ((fun (x : ℝ → ℝ) => PiecewiseConstantOn.RS_integ x I α) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I})

theorem Chapter11.le_lower_RS_integral {f : ℝ → ℝ} {I : BoundedInterval} {M : ℝ} (h : ∀ x ∈ ↑I, |f x| ≤ M) {α : ℝ → ℝ} (hα : Monotone α) : -M * α[I]ₗ ≤ lower_RS_integral f I α

theorem Chapter11.lower_RS_integral_le_upper {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) : lower_RS_integral f I α ≤ upper_RS_integral f I α

theorem Chapter11.RS_upper_integral_le {f : ℝ → ℝ} {I : BoundedInterval} {M : ℝ} (h : ∀ x ∈ ↑I, |f x| ≤ M) {α : ℝ → ℝ} (hα : Monotone α) : upper_RS_integral f I α ≤ M * α[I]ₗ

theorem Chapter11.upper_RS_integral_le_integ {f g : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) (hfg : MajorizesOn g f I) (hg : PiecewiseConstantOn g I) {α : ℝ → ℝ} (hα : Monotone α) : upper_RS_integral f I α ≤ PiecewiseConstantOn.RS_integ g I α

theorem Chapter11.integ_le_lower_RS_integral {f h : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) (hfh : MinorizesOn h f I) (hg : PiecewiseConstantOn h I) {α : ℝ → ℝ} (hα : Monotone α) : PiecewiseConstantOn.RS_integ h I α ≤ lower_RS_integral f I α

theorem Chapter11.lt_of_gt_upper_RS_integral {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) {X : ℝ} (hX : upper_RS_integral f I α < X) : ∃ (g : ℝ → ℝ), MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X

theorem Chapter11.gt_of_lt_lower_RS_integral {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) {X : ℝ} (hX : X < lower_RS_integral f I α) : ∃ (h : ℝ → ℝ), MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α

@[reducible, inline]

noncomputable abbrev Chapter11.RS_integ (f : ℝ → ℝ) (I : BoundedInterval) (α : ℝ → ℝ) : ℝ

Аналог визначення 11.3.4

Equations

• Chapter11.RS_integ f I α = Chapter11.upper_RS_integral f I α

@[reducible, inline]

noncomputable abbrev Chapter11.RS_IntegrableOn (f : ℝ → ℝ) (I : BoundedInterval) (α : ℝ → ℝ) : Prop

Equations

• Chapter11.RS_IntegrableOn f I α = (Chapter9.BddOn f ↑I ∧ Chapter11.lower_RS_integral f I α = Chapter11.upper_RS_integral f I α)

theorem Chapter11.upper_RS_integral_eq_upper_integral (f : ℝ → ℝ) (I : BoundedInterval) : (upper_RS_integral f I fun (x : ℝ) => x) = upper_integral f I

Аналог різних складових Леми 11.3.3

theorem Chapter11.lower_RS_integral_eq_lower_integral (f : ℝ → ℝ) (I : BoundedInterval) : (lower_RS_integral f I fun (x : ℝ) => x) = lower_integral f I

theorem Chapter11.RS_integ_eq_integ (f : ℝ → ℝ) (I : BoundedInterval) : (RS_integ f I fun (x : ℝ) => x) = integ f I

theorem Chapter11.RS_IntegrableOn_iff_IntegrableOn (f : ℝ → ℝ) (I : BoundedInterval) : (RS_IntegrableOn f I fun (x : ℝ) => x) ↔ IntegrableOn f I

theorem Chapter11.RS_integ_of_uniform_cts {I : BoundedInterval} {f : ℝ → ℝ} (hf : UniformContinuousOn f ↑I) {α : ℝ → ℝ} (hα : Monotone α) : RS_IntegrableOn f I α

Вправа 11.8.4

theorem Chapter11.RS_integ_with_sign (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc (-1) 1)) : RS_IntegrableOn f (BoundedInterval.Icc (-1) 1) Real.sign ∧ (RS_integ f (BoundedInterval.Icc (-1) 1) fun (x : ℝ) => -x.sign) = 2 * f 0

Вправа 11.8.5

theorem Chapter11.RS_integ_of_piecewise_const {f : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) {α : ℝ → ℝ} (hα : Monotone α) : RS_IntegrableOn f I α ∧ RS_integ f I α = PiecewiseConstantOn.RS_integ f I α

Аналог леми 11.3.7