Аналіз I, Розділ 11.10: Наслідки фундаментальних теорем

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

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

• Інтегрування частинами

theorem Chapter11.integ_of_mul_deriv {a b : ℝ} (hab : a ≤ b) {F G : ℝ → ℝ} (hF : DifferentiableOn ℝ F ↑(BoundedInterval.Icc a b)) (hG : DifferentiableOn ℝ G ↑(BoundedInterval.Icc a b)) (hF' : IntegrableOn (derivWithin F ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b)) (hG' : IntegrableOn (derivWithin G ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b)) : integ (F * derivWithin G ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b) = F b * G b - F a * G a - integ (G * derivWithin F ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b)

Твердження 11.10.1 (Формула інтегрування частинами) / Вправа 11.10.1

theorem Chapter11.PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv {a b : ℝ} {α f : ℝ → ℝ} (hα_diff : DifferentiableOn ℝ α ↑(BoundedInterval.Icc a b)) (hαcont : Continuous α) (hα' : IntegrableOn (derivWithin α ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b)) (hf : PiecewiseConstantOn f (BoundedInterval.Icc a b)) : IntegrableOn (f * derivWithin α ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b) ∧ Chapter11.integ (f * derivWithin α ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b) = RS_integ f (BoundedInterval.Icc a b) α

Теорема 11.10.2. Need to add continuity of α due to our conventions on α-length

theorem Chapter11.RS_integ_eq_integ_of_mul_deriv {a b : ℝ} (hab : a < b) {α f : ℝ → ℝ} (hα : Monotone α) (hα_diff : DifferentiableOn ℝ α ↑(BoundedInterval.Icc a b)) (hαcont : Continuous α) (hα' : IntegrableOn (derivWithin α ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b)) (hf : RS_IntegrableOn f (BoundedInterval.Icc a b) α) : IntegrableOn (f * derivWithin α ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b) ∧ integ (f * derivWithin α ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b) = RS_integ f (BoundedInterval.Icc a b) α

Наслідок 11.10.3

theorem Chapter11.PiecewiseConstantOn.RS_integ_of_comp {a b : ℝ} (hab : a < b) {φ f : ℝ → ℝ} (hφ_cont : Continuous φ) (hφ_mono : Monotone φ) (hf : PiecewiseConstantOn f (BoundedInterval.Icc (φ a) (φ b))) : PiecewiseConstantOn (f ∘ φ) (BoundedInterval.Icc a b) ∧ RS_integ (f ∘ φ) (BoundedInterval.Icc a b) φ = integ f (BoundedInterval.Icc (φ a) (φ b))

Лема 11.10.5 / Вправа 11.10.2

theorem Chapter11.RS_integ_of_comp {a b : ℝ} (hab : a < b) {φ f : ℝ → ℝ} (hφ_cont : Continuous φ) (hφ_mono : Monotone φ) (hf : IntegrableOn f (BoundedInterval.Icc (φ a) (φ b))) : RS_IntegrableOn (f ∘ φ) (BoundedInterval.Icc a b) φ ∧ RS_integ (f ∘ φ) (BoundedInterval.Icc a b) φ = integ f (BoundedInterval.Icc (φ a) (φ b))

Твердження 11.10.6 (Формула зміни змінної II)

theorem Chapter11.integ_of_comp {a b : ℝ} (hab : a < b) {φ f : ℝ → ℝ} (hφ_diff : DifferentiableOn ℝ φ ↑(BoundedInterval.Icc a b)) (hφ_cont : Continuous φ) (hφ_mono : Monotone φ) (hφ' : IntegrableOn (derivWithin φ ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b)) (hf : IntegrableOn f (BoundedInterval.Icc (φ a) (φ b))) : IntegrableOn (f ∘ φ * derivWithin φ ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b) ∧ integ (f ∘ φ * derivWithin φ ↑(BoundedInterval.Icc a b)) (BoundedInterval.Icc a b) = integ f (BoundedInterval.Icc (φ a) (φ b))

Твердження 11.10.7 (Формула зміни змінної III)