@[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₀ = (Filter.map f (nhdsWithin x₀ (Set.Ioi x₀))).lim

@[reducible, inline]

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

Equations

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

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.α_length α (Chapter11.BoundedInterval.Icc a b) = if a ≤ b then Chapter11.right_lim α b - Chapter11.left_lim α a else 0
• Chapter11.α_length α (Chapter11.BoundedInterval.Ico a b) = if a ≤ b then Chapter11.left_lim α b - Chapter11.left_lim α a else 0
• Chapter11.α_length α (Chapter11.BoundedInterval.Ioc a b) = if a ≤ b then Chapter11.right_lim α b - Chapter11.right_lim α a else 0
• Chapter11.α_length α (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.

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

@[simp]

theorem Chapter11.α_length_of_pt {α : ℝ → ℝ} (a : ℝ) : α_length α (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)) : α_length α I = α I.b - α I.a

@[simp]

theorem Chapter11.α_len_of_id (I : BoundedInterval) : α_length (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 ∧ ∀ (α : ℝ → ℝ), Chapter11.α_length α K = Chapter11.α_length α I + Chapter11.α_length α 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, α_length α J = α_length α 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 * Chapter11.α_length α 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 ^ 2) = 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 ≤ α_length α 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.3

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.3

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.3

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

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

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

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

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.3

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.3

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.3

@[reducible, inline]

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

Analogue of Definition 11.3.2 (Upper 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 * α_length α 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 * α_length α 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 * α_length α 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 * α_length α 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) Real.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