Analysis I, Section 11.8: The Riemann-Stieltjes integral

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:

• Definition of α-length.
• The piecewise constant Riemann-Stieltjes integral.
• The full Riemann-Stieltjes integral.

Technical notes:

• In Lean it is more convenient to make definitions such as α-length and the Riemann-Stieltjes integral totally defined, thus assigning "junk" values to the cases where the definition is not intended to be applied. For the definition of α-length, the definition is intended to be applied in contexts where left and right limits exist, and the function is extended by constants to the left and right of its intended domain of definition; for instance, if a function f is defined on Icc 0 1, then it is intended that f x = f 1 for all x ≥ 1 and f x = f 0 for all x ≤ 0; in particular, at a right endpoint, the value of a function is intended to agree with its right limit, and similarly for the left endpoint, although we do not enforce this in our definition of α-length. (For functions defined on open intervals, the extension is immaterial.)
• The notion of α-length and piecewise constant Riemann-Stieltjes integral is intended for situations where left and right limits exist, such as for monotone functions or continuous functions, though technically they make sense without these hypotheses. The full Riemann-Stieltjes integral is intended for functions that are of bounded variation, though we shall restrict attention to the special case of monotone increasing functions for the most part.

@[reducible, inline]

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

Left and right limits. A junk value is assigned if the limit does not exist.

Equations

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

@[reducible, inline]

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

Equations

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

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

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

@[reducible, inline]

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

Equations

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

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

Right limits exist for continuous functions

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

Left limits exist for continuous functions

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

No jump for continuous functions

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

Right limits exist for monotone functions

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

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

Left limits exist for monotone functions

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

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

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

@[reducible, inline]

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

Definition 11.8.1

Equations

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

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

Equations

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

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

Pretty printer defined by notation3 command.

Equations

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

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

@[simp]

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

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

@[simp]

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

Example 11.8.3

@[reducible, inline]

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

An improved version of BoundedInterval.joins that also controls α-length.

Equations

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

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

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

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

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

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

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

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

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

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

Theorem 11.8.4 / Exercise 11.8.1

@[reducible, inline]

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

Definition 11.8.5 (Piecewise constant RS integral)

Equations

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

@[reducible, inline]

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

Example 11.8.6

Equations

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

@[reducible, inline]

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

Equations

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

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

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

Example 11.8.7

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

Analogue of Proposition 11.2.13

@[reducible, inline]

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

Equations

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

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

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

α-length non-negative when α monotone

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

Analogue of Theorem 11.2.16 (a) (Laws of integration) / Exercise 11.8.3

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

Analogue of Theorem 11.2.16 (b) (Laws of integration) / Exercise 11.8.3

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

Theorem 11.8.8 (c) (Laws of RS integration) / Exercise 11.8.8

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

Theorem 11.8.8 (d) (Laws of RS integration) / Exercise 11.8.8

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

Theorem 11.8.8 (e) (Laws of RS integration) / Exercise 11.8.8

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

Theorem 11.8.8 (f) (Laws of RS integration) / Exercise 11.8.8

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

Theorem 11.8.8 (f) (Laws of RS integration) / Exercise 11.8.8

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

Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.8

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

Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.8

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

Theorem 11.8.8 (h) (Laws of RS integration) / Exercise 11.8.8

@[reducible, inline]

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

Analogue of Definition 11.3.2 (Uppper and lower Riemann integrals )

Equations

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

@[reducible, inline]

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

Analogue of Definition 11.3.4

Equations

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

@[reducible, inline]

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

Equations

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

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

Analogue of various components of Lemma 11.3.3

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

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

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

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

Exercise 11.8.4

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

Exercise 11.8.5

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

Analogue of Lemma 11.3.7