Imports
import Mathlib.Tactic
import Analysis.Section_9_6
import Analysis.Section_10_3
import Analysis.Section_11_9Analysis 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
namespace Chapter11open BoundedInterval Chapter9 Chapter10Proposition 11.10.1 (Integration by parts formula) / Exercise 11.10.1
theorem integ_of_mul_deriv {a b:ℝ} (hab: a ≤ b) {F G: ℝ → ℝ}
(hF: DifferentiableOn ℝ F (Icc a b)) (hG : DifferentiableOn ℝ G (Icc a b))
(hF': IntegrableOn (derivWithin F (Icc a b)) (Icc a b))
(hG': IntegrableOn (derivWithin G (Icc a b)) (Icc a b)) :
integ (F * derivWithin G (Icc a b)) (Icc a b) = F b * G b - F a * G a -
integ (G * derivWithin F (Icc a b)) (Icc a b) := a:ℝb:ℝhab:a ≤ bF:ℝ → ℝG:ℝ → ℝhF:DifferentiableOn ℝ F ↑(Icc a b)hG:DifferentiableOn ℝ G ↑(Icc a b)hF':IntegrableOn (derivWithin F ↑(Icc a b)) (Icc a b)hG':IntegrableOn (derivWithin G ↑(Icc a b)) (Icc a b)⊢ integ (F * derivWithin G ↑(Icc a b)) (Icc a b) = F b * G b - F a * G a - integ (G * derivWithin F ↑(Icc a b)) (Icc a b)
All goals completed! 🐙
Theorem 11.10.2. Need to add continuity of α due to our conventions on α_length
theorem PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv
{a b:ℝ} {α f:ℝ → ℝ}
(hα_diff: DifferentiableOn ℝ α (Icc a b)) (hαcont: Continuous α)
(hα': IntegrableOn (derivWithin α (Icc a b)) (Icc a b))
(hf: PiecewiseConstantOn f (Icc a b)) :
IntegrableOn (f * derivWithin α (Icc a b)) (Icc a b) ∧
Chapter11.integ (f * derivWithin α (Icc a b)) (Icc a b) = RS_integ f (Icc a b) α := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:PiecewiseConstantOn f (Icc a b)⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
Chapter11.integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
-- This proof is adapted from the structure of the original text.
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)⊢ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f P⊢ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f P⊢ ∑ J ∈ P.intervals, Chapter11.integ (f * α') J = PiecewiseConstantWith.RS_integ f P α
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f P⊢ ∀ x ∈ P.intervals, Chapter11.integ (f * α') x = constant_value_on f ↑x * α_length α x; intro J a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Chapter11.integ (f * α') J = constant_value_on f ↑J * α_length α J
calc
_ = Chapter11.integ ((constant_value_on f (J:Set ℝ)) • α') J := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Chapter11.integ (f * α') J = Chapter11.integ (constant_value_on f ↑J • α') J
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Set.EqOn (f * α') (constant_value_on f ↑J • α') ↑J; intro x a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalsx:ℝhx:x ∈ ↑J⊢ (f * α') x = (constant_value_on f ↑J • α') x
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalsx:ℝhx:x ∈ ↑J⊢ f x * α' x = constant_value_on f ↑J * α' x; a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalsx:ℝhx:x ∈ ↑J⊢ f x = constant_value_on f ↑J
All goals completed! 🐙
_ = constant_value_on f (J:Set ℝ) * Chapter11.integ α' J := ((hα'.mono' (P.contains _ hJ)).smul _).2
_ = _ := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * Chapter11.integ α' J = constant_value_on f ↑J * α_length α J
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Chapter11.integ α' J = α_length α J
have hJsub (hJab : J.a ≤ J.b) : J ⊆ Ioo (J.a - 1) (J.b + 1) :=
(subset_Icc J).trans (a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJab:J.a ≤ J.b⊢ Icc J.a J.b ⊆ Ioo (J.a - 1) (J.b + 1) All goals completed! 🐙)
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:0 = J.length⊢ Chapter11.integ α' J = α_length α Ja:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:0 < J.length⊢ Chapter11.integ α' J = α_length α J
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:0 = J.length⊢ Chapter11.integ α' J = α_length α J a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:0 = J.length⊢ 0 = α_length α J
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b < J.a ∨ J.b - J.a = 0⊢ 0 = α_length α J; a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b < J.a⊢ 0 = α_length α Ja:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ 0 = α_length α J
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b < J.a⊢ 0 = α_length α J All goals completed! 🐙
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ 0 = α J.b - α J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.a - 1 < J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.a ≤ J.ba:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.b < J.b + 1a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.a ≤ J.b a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ 0 = α J.b - α J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.a - 1 < J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.a ≤ J.ba:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.b < J.b + 1a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.b - J.a = 0⊢ J.a ≤ J.b All goals completed! 🐙
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.b⊢ Chapter11.integ α' J = α_length α J
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.b⊢ Chapter11.integ α' J = α J.b - α J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.b⊢ J.a - 1 < J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.b⊢ J.a ≤ J.ba:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.b⊢ J.b < J.b + 1a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.b⊢ J.a ≤ J.b
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.b⊢ Chapter11.integ α' J = α J.b - α J.a have : Icc J.a J.b ⊆ Icc a b := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * Chapter11.integ α' J = constant_value_on f ↑J * α_length α J
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.bthis:closure ↑(Ioo J.a J.b) ⊆ closure ↑(Icc a b)⊢ Icc J.a J.b ⊆ Icc a b
simpa [closure_Ioo (show J.a ≠ J.b a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * Chapter11.integ α' J = constant_value_on f ↑J * α_length α J All goals completed! 🐙), subset_iff] using this
calc
_ = Chapter11.integ α' (Icc J.a J.b) := (hα'.mono' this).eq (subset_Icc J) rfl rfl
_ = _ := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.bthis:Icc J.a J.b ⊆ Icc a b⊢ Chapter11.integ α' (Icc J.a J.b) = α J.b - α J.a
convert integ_eq_antideriv_sub (a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.bthis:Icc J.a J.b ⊆ Icc a b⊢ J.a ≤ J.b All goals completed! 🐙) (hα'.mono' this) _
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.bthis:Icc J.a J.b ⊆ Icc a b⊢ ∀ x ∈ Icc a b, HasDerivWithinAt α (α' x) (↑(Icc a b)) x
a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hf_integ:IntegrableOn f (Icc a b)hfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:J.a ≤ J.b → J ⊆ Ioo (J.a - 1) (J.b + 1)hJab:J.a < J.bthis:Icc J.a J.b ⊆ Icc a bx✝:ℝa✝:x✝ ∈ Icc a b⊢ HasDerivWithinAt α (α' x✝) (↑(Icc a b)) x✝; All goals completed! 🐙
all_goals All goals completed! 🐙Corollary 11.10.3
theorem RS_integ_eq_integ_of_mul_deriv
{a b:ℝ} (hab: a < b) {α f:ℝ → ℝ} (hα: Monotone α)
(hα_diff: DifferentiableOn ℝ α (Icc a b)) (hαcont: Continuous α)
(hα': IntegrableOn (derivWithin α (Icc a b)) (Icc a b))
(hf: RS_IntegrableOn f (Icc a b) α) :
IntegrableOn (f * derivWithin α (Icc a b)) (Icc a b) ∧
integ (f * derivWithin α (Icc a b)) (Icc a b) = RS_integ f (Icc a b) α := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
-- This proof is adapted from the structure of the original text.
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
have hfα'_bound: BddOn (f * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ M⊢ BddOn (f * α') ↑(Icc a b); a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ MN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ N⊢ BddOn (f * α') ↑(Icc a b)
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ MN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ N⊢ ∀ x ∈ ↑(Icc a b), |(f * α') x| ≤ M * N; intro x a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ MN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ Nx:ℝhx:x ∈ ↑(Icc a b)⊢ |(f * α') x| ≤ M * N; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ Nx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ M⊢ |(f * α') x| ≤ M * N; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ MhN:|α' x| ≤ N⊢ |(f * α') x| ≤ M * N
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ MhN:|α' x| ≤ N⊢ |f x| * |α' x| ≤ M * N; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ MhN:|α' x| ≤ N⊢ 0 ≤ M; All goals completed! 🐙
have hα'_nonneg : MajorizesOn α' 0 (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
intro x a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:x ∈ ↑(Icc a b)⊢ 0 x ≤ α' x
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:x ∈ ↑(Icc a b)⊢ ClusterPt x (Filter.principal (↑(Icc a b) \ {x}))
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:x ∈ ↑(Icc a b)⊢ x ∈ closure (↑(Icc a b) \ {x})
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ b⊢ x ∈ closure (↑(Icc a b) \ {x})
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (↑(Icc a b) \ {x})a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ x ∈ closure (↑(Icc a b) \ {x})
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (↑(Icc a b) \ {x}) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (Set.Ico a x)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ Set.Ico a x ⊆ ↑(Icc a b) \ {x}
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (Set.Ico a x) All goals completed! 🐙
intro _ a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a < xa✝¹:ℝa✝:a✝¹ ∈ Set.Ico a x⊢ a✝¹ ∈ ↑(Icc a b) \ {x}; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αα':ℝ → ℝ := derivWithin α ↑(Icc a b)x:ℝa✝¹:ℝhα_diff:DifferentiableOn ℝ α (Set.Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αhα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') (Set.Icc a b)hx:a ≤ x ∧ x ≤ bh:a < xa✝:a ≤ a✝¹ ∧ a✝¹ < x⊢ a✝¹ ≤ b ∧ ¬a✝¹ = x; All goals completed! 🐙
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ x ∈ closure (Set.Ioc x b)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ Set.Ioc x b ⊆ ↑(Icc a b) \ {x}
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ x ∈ closure (Set.Ioc x b) All goals completed! 🐙
intro _ a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)x:ℝhx:a ≤ x ∧ x ≤ bh:a = xa✝¹:ℝa✝:a✝¹ ∈ Set.Ioc x b⊢ a✝¹ ∈ ↑(Icc a b) \ {x}; All goals completed! 🐙
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) α⊢ IntegrableOn (f * α') (Icc a b) ∧ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
have h1 : RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) α⊢ ∀ ε > 0, RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b); intro ε a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αε:ℝhε:ε > 0⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b)
have ⟨ h, hhminor, hhconst, hh ⟩ :=
gt_of_lt_lower_RS_integral hf.1 hα (show RS_integ f (Icc a b) α - ε < lower_RS_integral f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙)
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αε:ℝhε:ε > 0h:ℝ → ℝhhminor:MinorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:RS_integ f (Icc a b) α - ε < PiecewiseConstantOn.RS_integ h (Icc a b) αthis:IntegrableOn (h * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (h * derivWithin α ↑(Icc a b)) (Icc a b) = PiecewiseConstantOn.RS_integ h (Icc a b) α⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b)
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αε:ℝhε:ε > 0h:ℝ → ℝhhminor:MinorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:RS_integ f (Icc a b) α - ε < integ (h * derivWithin α ↑(Icc a b)) (Icc a b)this:IntegrableOn (h * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (h * derivWithin α ↑(Icc a b)) (Icc a b) = PiecewiseConstantOn.RS_integ h (Icc a b) α⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b)
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αε:ℝhε:ε > 0h:ℝ → ℝhhminor:MinorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:RS_integ f (Icc a b) α - ε < integ (h * derivWithin α ↑(Icc a b)) (Icc a b)this:lower_integral (h * α') (Icc a b) = integ (h * α') (Icc a b)⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b)
have why : lower_integral (h * α') (Icc a b) ≤ lower_integral (f * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
All goals completed! 🐙
All goals completed! 🐙
have h2 : upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)⊢ ∀ (ε : ℝ), 0 < ε → upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε; intro ε a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)ε:ℝhε:0 < ε⊢ upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε
have ⟨ h, hhmajor, hhconst, hh ⟩ :=
lt_of_gt_upper_RS_integral hf.1 hα (show upper_RS_integral f (Icc a b) α + ε > RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙)
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)ε:ℝhε:0 < εh:ℝ → ℝhhmajor:MajorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:PiecewiseConstantOn.RS_integ h (Icc a b) α < upper_RS_integral f (Icc a b) α + εthis:IntegrableOn (h * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (h * derivWithin α ↑(Icc a b)) (Icc a b) = PiecewiseConstantOn.RS_integ h (Icc a b) α⊢ upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)ε:ℝhε:0 < εh:ℝ → ℝhhmajor:MajorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:integ (h * derivWithin α ↑(Icc a b)) (Icc a b) < upper_RS_integral f (Icc a b) α + εthis:IntegrableOn (h * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (h * derivWithin α ↑(Icc a b)) (Icc a b) = PiecewiseConstantOn.RS_integ h (Icc a b) α⊢ upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε
have why : upper_integral (f * α') (Icc a b) ≤ upper_integral (h * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧
integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α
All goals completed! 🐙
All goals completed! 🐙
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)h2:upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) αh3:lower_integral (f * α') (Icc a b) ≤ upper_integral (f * α') (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α
a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)h2:upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) αh3:lower_integral (f * α') (Icc a b) ≤ upper_integral (f * α') (Icc a b)⊢ lower_integral (f * α') (Icc a b) = upper_integral (f * α') (Icc a b)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)h2:upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) αh3:lower_integral (f * α') (Icc a b) ≤ upper_integral (f * α') (Icc a b)⊢ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)h2:upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) αh3:lower_integral (f * α') (Icc a b) ≤ upper_integral (f * α') (Icc a b)⊢ lower_integral (f * α') (Icc a b) = upper_integral (f * α') (Icc a b)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin α ↑(Icc a b)hα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') ↑(Icc a b)hα'_nonneg:MajorizesOn α' 0 (Icc a b)h0:lower_RS_integral f (Icc a b) α = upper_RS_integral f (Icc a b) αh1:RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b)h2:upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) αh3:lower_integral (f * α') (Icc a b) ≤ upper_integral (f * α') (Icc a b)⊢ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙Lemma 11.10.5 / Exercise 11.10.2
theorem PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ → ℝ}
(hφ_cont: Continuous φ) (hφ_mono: Monotone φ) (hf: PiecewiseConstantOn f (Icc (φ a) (φ b))) :
PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ =
integ f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
-- This proof is adapted from the structure of the original text.
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'P:Partition (Icc (φ a) (φ b)) := P'.remove_empty⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
replace hf : PiecewiseConstantWith f P := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
intro J a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyJ:BoundedIntervalhJ:J ∈ P⊢ ConstantOn f ↑J; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyJ:BoundedIntervalhJ:{x | (↑P'.intervals).Mem x ∧ (↑x).Nonempty}.Mem J⊢ ConstantOn f ↑J; All goals completed! 🐙
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f P⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = PiecewiseConstantWith.integ f P
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f P⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧
RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧
RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
have hφ_inv_bounded (J: P.intervals) : Bornology.IsBounded (φ_inv J) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}J:↥P.intervals⊢ φ_inv J ⊆ Set.Icc a b; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}J:↥P.intervalsa✝:ℝ⊢ a✝ ∈ φ_inv J → a✝ ∈ Set.Icc a b; All goals completed! 🐙
have hφ_inv_connected (J: P.intervals) : (φ_inv J).OrdConnected := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choose⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧
RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧
RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
have hφ_inv_nonempty (J:P.intervals) : (φ_inv J).Nonempty := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙
have hφ_inv_const {J:P.intervals} : ConstantOn (f ∘ φ) (φ_inv' J) ∧ constant_value_on (f ∘ φ) (φ_inv' J) = constant_value_on f J := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
All goals completed! 🐙
set Q : Partition (Icc a b) := {
intervals := .image φ_inv' .univ
exists_unique x := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑Jx:ℝ⊢ x ∈ Icc a b → ∃! J, J ∈ Finset.image φ_inv' Finset.univ ∧ x ∈ J All goals completed! 🐙
contains K hK := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JK:BoundedIntervalhK:K ∈ Finset.image φ_inv' Finset.univ⊢ K ⊆ Icc a b All goals completed! 🐙
}
have hfφ_piecewise : PiecewiseConstantWith (f ∘ φ) Q := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
All goals completed! 🐙
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧
RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ PiecewiseConstantWith.RS_integ (f ∘ φ) Q φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ ∑ J ∈ Q.intervals, constant_value_on (f ∘ φ) ↑J * α_length φ J = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ ∑ x, constant_value_on (f ∘ φ) ↑(φ_inv' x) * α_length φ (φ_inv' x) = ∑ i, constant_value_on f ↑↑i * (↑i).lengtha:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ Set.InjOn φ_inv' ↑Finset.univ
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ ∑ x, constant_value_on (f ∘ φ) ↑(φ_inv' x) * α_length φ (φ_inv' x) = ∑ i, constant_value_on f ↑↑i * (↑i).length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)⊢ ∀ x ∈ Finset.univ, constant_value_on (f ∘ φ) ↑(φ_inv' x) * α_length φ (φ_inv' x) = constant_value_on f ↑↑x * (↑x).length
intro J a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝:J ∈ Finset.univ⊢ constant_value_on (f ∘ φ) ↑(φ_inv' J) * α_length φ (φ_inv' J) = constant_value_on f ↑↑J * (↑J).length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝:J ∈ Finset.univ⊢ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑Ja:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝:J ∈ Finset.univ⊢ α_length φ (φ_inv' J) = (↑J).length
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝:J ∈ Finset.univ⊢ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑J All goals completed! 🐙
All goals completed! 🐙
intro J a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝:J ∈ ↑Finset.univ⊢ ∀ ⦃x₂ : ↥P.intervals⦄, x₂ ∈ ↑Finset.univ → φ_inv' J = φ_inv' x₂ → J = x₂ a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝:J ∈ ↑Finset.univK:↥P.intervals⊢ K ∈ ↑Finset.univ → φ_inv' J = φ_inv' K → J = K a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univ⊢ φ_inv' J = φ_inv' K → J = K a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' K⊢ J = K
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.some⊢ J = K
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:x ∈ φ_inv J⊢ J = K
have h2 : x ∈ φ_inv K := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) rwa [hφ_inv' J, hJK, ←hφ_inv' Ka:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:x ∈ φ_inv K⊢ x ∈ φ_inv K at h1
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑K⊢ J = K
have h3 : φ x ∈ Icc (φ a) (φ b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kthis:↑J ⊆ Icc (φ a) (φ b)⊢ φ x ∈ Icc (φ a) (φ b)
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kthis:↑↑J ⊆ ↑(Icc (φ a) (φ b))⊢ φ x ∈ ↑(Icc (φ a) (φ b))
All goals completed! 🐙
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:φ x ∈ Icc (φ a) (φ b)⊢ ↑J = ↑K; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:φ x ∈ Icc (φ a) (φ b)⊢ ↑J ∈ P.intervals ∧ φ x ∈ ↑Ja:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:φ x ∈ Icc (φ a) (φ b)⊢ ↑K ∈ P.intervals ∧ φ x ∈ ↑K a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:φ x ∈ Icc (φ a) (φ b)⊢ ↑J ∈ P.intervals ∧ φ x ∈ ↑Ja:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Partition (Icc (φ a) (φ b)) := P'.remove_emptyhf:PiecewiseConstantWith f Pφ_inv:↥P.intervals → Set ℝ := fun J ↦ {x | x ∈ Set.Icc a b ∧ φ x ∈ ↑↑J}hφ_inv_bounded:∀ (J : ↥P.intervals), Bornology.IsBounded (φ_inv J)hφ_inv_connected:∀ (J : ↥P.intervals), (φ_inv J).OrdConnectedφ_inv':↥P.intervals → BoundedInterval := fun J ↦ ⋯.choosehφ_inv':∀ (J : ↥P.intervals), φ_inv J = ↑(φ_inv' J)hφ_inv_nonempty:∀ (J : ↥P.intervals), (φ_inv J).Nonemptyhφ_inv_const:∀ {J : ↥P.intervals}, ConstantOn (f ∘ φ) ↑(φ_inv' J) ∧ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑JQ:Partition (Icc a b) := { intervals := Finset.image φ_inv' Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:PiecewiseConstantWith (f ∘ φ) Qhfφ_piecewise':PiecewiseConstantOn (f ∘ φ) (Icc a b)J:↥P.intervalsa✝¹:J ∈ ↑Finset.univK:↥P.intervalsa✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := ⋯.someh1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:φ x ∈ Icc (φ a) (φ b)⊢ ↑K ∈ P.intervals ∧ φ x ∈ ↑K All goals completed! 🐙Proposition 11.10.6 (Change of variables formula II)
theorem RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ}
(hφ_cont: Continuous φ) (hφ_mono: Monotone φ) (hf: IntegrableOn f (Icc (φ a) (φ b))) :
RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧
RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
-- This proof is adapted from the structure of the original text.
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
have hfφ_bdd : BddOn (f ∘ φ) (Icc a b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
All goals completed! 🐙
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
have hupper : upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))⊢ ∀ (ε : ℝ), 0 < ε → upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε
intro ε a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))ε:ℝhε:0 < ε⊢ upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε
choose f_up hf_upmajor hf_upconst hf_up using lt_of_gt_upper_integral hf.1 (show upper_integral f (Icc (φ a) (φ b)) + ε > integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙)
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b)) < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))⊢ upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))⊢ upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε
have : MajorizesOn (f_up ∘ φ) (f ∘ φ) (Icc a b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) intro _ a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))x✝:ℝa✝:x✝ ∈ ↑(Icc a b)⊢ (f ∘ φ) x✝ ≤ (f_up ∘ φ) x✝; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)a✝:a ≤ x✝ ∧ x✝ ≤ b⊢ f (φ x✝) ≤ f_up (φ x✝); a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)a✝:a ≤ x✝ ∧ x✝ ≤ b⊢ φ x✝ ∈ ↑(Icc (φ a) (φ b)); All goals completed! 🐙
All goals completed! 🐙
have hlower : lower_integral f (Icc (φ a) (φ b)) ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))⊢ ∀ ε > 0, lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ
intro ε a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))ε:ℝhε:ε > 0⊢ lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ
choose f_low hf_lowminor hf_lowconst hf_low using gt_of_lt_lower_integral hf.1 (show lower_integral f (Icc (φ a) (φ b)) - ε < lower_integral f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙)
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))ε:ℝhε:ε > 0f_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))hpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))⊢ lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))ε:ℝhε:ε > 0f_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))⊢ lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ
have : MinorizesOn (f_low ∘ φ) (f ∘ φ) (Icc a b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) intro _ a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))ε:ℝhε:ε > 0f_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))x✝:ℝa✝:x✝ ∈ ↑(Icc a b)⊢ (f_low ∘ φ) x✝ ≤ (f ∘ φ) x✝; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))ε:ℝf_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)hε:0 < εa✝:a ≤ x✝ ∧ x✝ ≤ b⊢ f_low (φ x✝) ≤ f (φ x✝); a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))ε:ℝf_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧
PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)hε:0 < εa✝:a ≤ x✝ ∧ x✝ ≤ b⊢ φ x✝ ∈ ↑(Icc (φ a) (φ b)); All goals completed! 🐙
All goals completed! 🐙
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))hlower:lower_integral f (Icc (φ a) (φ b)) ≤ lower_RS_integral (f ∘ φ) (Icc a b) φhle:lower_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_RS_integral (f ∘ φ) (Icc a b) φ⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))hlower:lower_integral f (Icc (φ a) (φ b)) ≤ lower_RS_integral (f ∘ φ) (Icc a b) φhle:lower_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_RS_integral (f ∘ φ) (Icc a b) φ⊢ lower_RS_integral (f ∘ φ) (Icc a b) φ = upper_RS_integral (f ∘ φ) (Icc a b) φa:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))hlower:lower_integral f (Icc (φ a) (φ b)) ≤ lower_RS_integral (f ∘ φ) (Icc a b) φhle:lower_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_RS_integral (f ∘ φ) (Icc a b) φ⊢ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))hlower:lower_integral f (Icc (φ a) (φ b)) ≤ lower_RS_integral (f ∘ φ) (Icc a b) φhle:lower_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_RS_integral (f ∘ φ) (Icc a b) φ⊢ lower_RS_integral (f ∘ φ) (Icc a b) φ = upper_RS_integral (f ∘ φ) (Icc a b) φa:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:BddOn f ↑(Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) ↑(Icc a b)heq:lower_integral f (Icc (φ a) (φ b)) = upper_integral f (Icc (φ a) (φ b))hupper:upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b))hlower:lower_integral f (Icc (φ a) (φ b)) ≤ lower_RS_integral (f ∘ φ) (Icc a b) φhle:lower_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_RS_integral (f ∘ φ) (Icc a b) φ⊢ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙Proposition 11.10.7 (Change of variables formula III)
theorem integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ}
(hφ_diff: DifferentiableOn ℝ φ (Icc a b))
(hφ_cont: Continuous φ) (hφ_mono: Monotone φ)
(hφ': IntegrableOn (derivWithin φ (Icc a b)) (Icc a b))
(hf: IntegrableOn f (Icc (φ a) (φ b))) :
IntegrableOn (f ∘ φ * derivWithin φ (Icc a b)) (Icc a b) ∧
integ (f ∘ φ * derivWithin φ (Icc a b)) (Icc a b) =
integ f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))⊢ IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧
integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))h1:RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))⊢ IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧
integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b))
a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))h1:RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))h2:IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧
integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = RS_integ (f ∘ φ) (Icc a b) φ⊢ IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧
integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b))
refine ⟨ h2.1, a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))h1:RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b))h2:IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧
integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = RS_integ (f ∘ φ) (Icc a b) φ⊢ integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b)) All goals completed! 🐙 ⟩/-- Exercise 11.10.3-/
example {a b:ℝ} (hab: a < b) {f: ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) :
IntegrableOn (fun x ↦ f (-x)) (Icc (-b) (-a)) ∧
integ (fun x ↦ f (-x)) (Icc (-b) (-a)) = -integ f (Icc a b) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)⊢ IntegrableOn (fun x ↦ f (-x)) (Icc (-b) (-a)) ∧ integ (fun x ↦ f (-x)) (Icc (-b) (-a)) = -integ f (Icc a b)
All goals completed! 🐙/- Exercise 11.10.4: state and prove a version of `integ_of_comp` in which `φ` is `Antitone` rather than `Monotone`. -/
end Chapter11