Аналіз I, Розділ 11.4: Основні властивості інтегралу Рімана

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

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

• Основні властивості інтегралу Рімана.

theorem Chapter11.IntegrableOn.add {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f + g) I ∧ integ (f + g) I = integ f I + integ g I

Теорема 11.4.1(a) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.smul {I : BoundedInterval} (c : ℝ) {f : ℝ → ℝ} (hf : IntegrableOn f I) : IntegrableOn (c • f) I ∧ integ (c • f) I = c * integ f I

Теорема 11.4.1(b) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.neg {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) : IntegrableOn (-f) I ∧ integ (-f) I = -integ f I

theorem Chapter11.IntegrableOn.sub {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f - g) I ∧ integ (f - g) I = integ f I - integ g I

Теорема 11.4.1(c) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.nonneg {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) (hf_nonneg : ∀ x ∈ I, 0 ≤ f x) : 0 ≤ integ f I

Теорема 11.4.1(d) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.mono {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) (h : MajorizesOn g f I) : integ f I ≤ integ g I

Теорема 11.4.1(e) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.const (c : ℝ) (I : BoundedInterval) : IntegrableOn (fun (x : ℝ) => c) I ∧ integ (fun (x : ℝ) => c) I = c * I.length

Теорема 11.4.1(f) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.const' {I : BoundedInterval} {f : ℝ → ℝ} (hf : ConstantOn f ↑I) : IntegrableOn f I ∧ integ f I = constant_value_on f ↑I * I.length

Теорема 11.4.1(f) / Вправа 11.4.1

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

Теорема 11.4.1 (g) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.of_extend' {I J : BoundedInterval} (hIJ : I ⊆ J) {f : ℝ → ℝ} (h : IntegrableOn f I) : integ (fun (x : ℝ) => if x ∈ I then f x else 0) J = integ f I

Теорема 11.4.1 (g) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.join {I J K : BoundedInterval} (hIJK : K.joins I J) {f : ℝ → ℝ} (h : IntegrableOn f K) : IntegrableOn f I ∧ IntegrableOn f J ∧ integ f K = integ f I + integ f J

Теорема 11.4.1 (h) (Закони інтегрування) / Вправа 11.4.1

theorem Chapter11.IntegrableOn.mono' {I J : BoundedInterval} (hIJ : J ⊆ I) {f : ℝ → ℝ} (h : IntegrableOn f I) : IntegrableOn f J

Варіант теореми 11.4.1(h), корисний у наступних розділах.

theorem Chapter11.IntegrableOn.eq {I J : BoundedInterval} (hIJ : J ⊆ I) (ha : J.a = I.a) (hb : J.b = I.b) {f : ℝ → ℝ} (h : IntegrableOn f I) : integ f J = integ f I

Ще один варіант теореми 11.4.1(h), корисний у наступних розділах.

theorem Chapter11.nonneg_of_le_const_mul_eps {x C : ℝ} (h : ∀ ε > 0, x ≤ C * ε) : x ≤ 0

Невелика корисна лема для міркувань типу «ε в запасі»

theorem Chapter11.IntegrableOn.max {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f ⊔ g) I

Теорема 11.4.3 (Максимум і мінімум зберігають інтегровність)

theorem Chapter11.IntegrableOn.min {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f ⊓ g) I

Теорема 11.4.5 / Вправа 11.4.3. Мета тут — отримати коротший доказ, ніж наведений вище.

theorem Chapter11.IntegrableOn.abs {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) : IntegrableOn |f| I

Наслідок 11.4.4

theorem Chapter11.integ_of_mul_nonneg {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) (hf_nonneg : MajorizesOn f 0 I) (hg_nonneg : MajorizesOn g 0 I) : IntegrableOn (f * g) I

Теорема 11.4.5 (Добутки зберігають інтегровність Рімана). Зручніше спочатку розглянути випадок невід'ємних функцій.

theorem Chapter11.integ_of_mul {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f * g) I

theorem Chapter11.IntegrableOn.split {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) (P : Partition I) : integ f I = ∑ J ∈ P.intervals, integ f J

Вправа 11.4.2