Analysis I, Section 11.10: Consequences of the fundamental theorems

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Integration by parts

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)

Proposition 11.10.1 (Integration by parts formula) / Exercise 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) α

Theorem 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) α

Corollary 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))

Lemma 11.10.5 / Exercise 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))

Proposition 11.10.6 (Change of variables formula 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))

Proposition 11.10.7 (Change of variables formula III)