Аналіз I, Глава 11.1

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:

• Bounded intervals and partitions
• Length of an interval; the lengths of a partition sum to the length of the interval

inductive Chapter11.BoundedInterval : Type

• Ioo (a b : ℝ) : BoundedInterval
• Icc (a b : ℝ) : BoundedInterval
• Ioc (a b : ℝ) : BoundedInterval
• Ico (a b : ℝ) : BoundedInterval

instance Chapter11.BoundedInterval.inst_coeSet : Coe BoundedInterval (Set ℝ)

There is a technical issue in that this coercion is not injective: the empty set is represented by multiple bounded intervals. This causes some of the statements in this section to be a little uglier than necessary.

Equations

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

instance Chapter11.BoundedInterval.instEmpty : EmptyCollection BoundedInterval

Equations

• Chapter11.BoundedInterval.instEmpty = { emptyCollection := Chapter11.BoundedInterval.Ioo 0 0 }

noncomputable instance Chapter11.BoundedInterval.decidableEq : DecidableEq BoundedInterval

This is to make Finsets of BoundedIntervals work properly

Equations

• Chapter11.BoundedInterval.decidableEq = instDecidableEqOfLawfulBEq

@[simp]

theorem Chapter11.BoundedInterval.set_Ioo (a b : ℝ) : (match Ioo a b with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) = Set.Ioo a b

@[simp]

theorem Chapter11.BoundedInterval.set_Icc (a b : ℝ) : (match Icc a b with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) = Set.Icc a b

@[simp]

theorem Chapter11.BoundedInterval.set_Ioc (a b : ℝ) : (match Ioc a b with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) = Set.Ioc a b

@[simp]

theorem Chapter11.BoundedInterval.set_Ico (a b : ℝ) : (match Ico a b with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) = Set.Ico a b

theorem Chapter11.BoundedInterval.ordConnected_iff (X : Set ℝ) : Bornology.IsBounded X ∧ X.OrdConnected ↔ ∃ (I : BoundedInterval), X = match I with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b

Лема 11.1.4 / Вправа 11.1.1

theorem Chapter11.BoundedInterval.inter (I J : BoundedInterval) : ∃ (K : BoundedInterval), ((match I with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) ∩ match J with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) = match K with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b

Наслідок 11.1.6 / Вправа 11.1.2

noncomputable instance Chapter11.BoundedInterval.instInter : Inter BoundedInterval

Equations

• Chapter11.BoundedInterval.instInter = { inter := fun (I J : Chapter11.BoundedInterval) => ⋯.choose }

@[simp]

theorem Chapter11.BoundedInterval.inter_eq (I J : BoundedInterval) : (match I ∩ J with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) = (match I with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) ∩ match J with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b

instance Chapter11.BoundedInterval.instMembership : Membership ℝ BoundedInterval

Equations

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

theorem Chapter11.BoundedInterval.mem_iff (I : BoundedInterval) (x : ℝ) : x ∈ I ↔ x ∈ match I with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b

instance Chapter11.BoundedInterval.instSubset : HasSubset BoundedInterval

Equations

• Chapter11.BoundedInterval.instSubset = { Subset := fun (I J : Chapter11.BoundedInterval) => ∀ x ∈ I, x ∈ J }

theorem Chapter11.BoundedInterval.subset_iff (I J : BoundedInterval) : I ⊆ J ↔ (match I with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) ⊆ match J with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b

@[reducible, inline]

abbrev Chapter11.BoundedInterval.a (I : BoundedInterval) : ℝ

Equations

• (Chapter11.BoundedInterval.Ioo a b).a = a
• (Chapter11.BoundedInterval.Icc a b).a = a
• (Chapter11.BoundedInterval.Ioc a b).a = a
• (Chapter11.BoundedInterval.Ico a b).a = a

@[reducible, inline]

abbrev Chapter11.BoundedInterval.b (I : BoundedInterval) : ℝ

Equations

• (Chapter11.BoundedInterval.Ioo a b).b = b
• (Chapter11.BoundedInterval.Icc a b).b = b
• (Chapter11.BoundedInterval.Ioc a b).b = b
• (Chapter11.BoundedInterval.Ico a b).b = b

theorem Chapter11.BoundedInterval.subset_Icc (I : BoundedInterval) : I ⊆ Icc I.a I.b

theorem Chapter11.BoundedInterval.Ioo_subset (I : BoundedInterval) : Ioo I.a I.b ⊆ I

instance Chapter11.BoundedInterval.instTrans : IsTrans BoundedInterval fun (x1 x2 : BoundedInterval) => x1 ⊆ x2

@[simp]

theorem Chapter11.BoundedInterval.mem_inter (I J : BoundedInterval) (x : ℝ) : x ∈ I ∩ J ↔ x ∈ I ∧ x ∈ J

@[reducible, inline]

abbrev Chapter11.BoundedInterval.length (I : BoundedInterval) : ℝ

Equations

• I.length = max (I.b - I.a) 0

def Chapter11.«term|___|ₗ» : Lean.ParserDescr

Using ||ₗ subscript here to not override ||

Equations

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

theorem Chapter11.BoundedInterval.length_of_empty {I : BoundedInterval} (hI : (match I with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) = ∅) : I.length = 0

theorem Chapter11.BoundedInterval.length_of_subsingleton {I : BoundedInterval} : Subsingleton ↑(match I with | Ioo a b => Set.Ioo a b | Icc a b => Set.Icc a b | Ioc a b => Set.Ioc a b | Ico a b => Set.Ico a b) ↔ I.length = 0

@[reducible, inline]

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

Equations

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

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)

structure Chapter11.Partition (I : BoundedInterval) : Type

• intervals : Finset BoundedInterval
• exists_unique (x : ℝ) (hx : x ∈ I) : ∃! J : BoundedInterval, J ∈ self.intervals ∧ x ∈ J
• contains (J : BoundedInterval) (hJ : J ∈ self.intervals) : J ⊆ I

theorem Chapter11.Partition.ext_iff {I : BoundedInterval} {x y : Partition I} : x = y ↔ x.intervals = y.intervals

theorem Chapter11.Partition.ext {I : BoundedInterval} {x y : Partition I} (intervals : x.intervals = y.intervals) : x = y

instance Chapter11.Partition.instMembership (I : BoundedInterval) : Membership BoundedInterval (Partition I)

Equations

• Chapter11.Partition.instMembership I = { mem := fun (P : Chapter11.Partition I) (J : Chapter11.BoundedInterval) => J ∈ P.intervals }

instance Chapter11.Partition.instBot (I : BoundedInterval) : Bot (Partition I)

Equations

• Chapter11.Partition.instBot I = { bot := { intervals := {I}, exists_unique := ⋯, contains := ⋯ } }

@[simp]

theorem Chapter11.Partition.intervals_of_bot (I : BoundedInterval) : ⊥.intervals = {I}

@[reducible, inline]

noncomputable abbrev Chapter11.Partition.join {I J K : BoundedInterval} (P : Partition I) (Q : Partition J) (h : K.joins I J) : Partition K

Equations

• P.join Q h = { intervals := P.intervals ∪ Q.intervals, exists_unique := ⋯, contains := ⋯ }

@[simp]

theorem Chapter11.Partition.intervals_of_join {I J K : BoundedInterval} {h : K.joins I J} (P : Partition I) (Q : Partition J) : (P.join Q h).intervals = P.intervals ∪ Q.intervals

@[reducible, inline]

noncomputable abbrev Chapter11.Partition.add_empty {I : BoundedInterval} (P : Partition I) : Partition I

Equations

• P.add_empty = { intervals := P.intervals ∪ {∅}, exists_unique := ⋯, contains := ⋯ }

@[simp]

theorem Chapter11.Partition.intervals_of_add_empty (I : BoundedInterval) (P : Partition I) : P.add_empty.intervals = P.intervals ∪ {∅}

theorem Chapter11.Partition.exist_right {I : BoundedInterval} (hI : I.a < I.b) (hI' : I.b ∉ I) {P : Partition I} : ∃ c ∈ Set.Ico I.a I.b, BoundedInterval.Ioo c I.b ∈ P ∨ BoundedInterval.Ico c I.b ∈ P

Вправа 11.1.3. The exercise only claims c ≤ b, but the stronger claim c < b is true and useful.

theorem Chapter11.Partition.sum_of_length (I : BoundedInterval) (P : Partition I) : ∑ J ∈ P.intervals, J.length = I.length

Теорема 11.1.13 (Length is finitely additive). Due to the excessive case analysis, simp only is used in place of simp in some places to speed up elaboration.

instance Chapter11.Partition.instLE (I : BoundedInterval) : LE (Partition I)

Визначення 11.1.14 (Finer and coarser partitions)

Equations

• Chapter11.Partition.instLE I = { le := fun (P P' : Chapter11.Partition I) => ∀ J ∈ P'.intervals, ∃ K ∈ P, J ⊆ K }

instance Chapter11.Partition.instPreOrder (I : BoundedInterval) : Preorder (Partition I)

Equations

• Chapter11.Partition.instPreOrder I = { toLE := Chapter11.Partition.instLE I, lt := fun (a b : Chapter11.Partition I) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }

instance Chapter11.Partition.instOrderBot (I : BoundedInterval) : OrderBot (Partition I)

Equations

• Chapter11.Partition.instOrderBot I = { toBot := Chapter11.Partition.instBot I, bot_le := ⋯ }

noncomputable instance Chapter11.Partition.instMax (I : BoundedInterval) : Max (Partition I)

Визначення 11.1.16 (Common refinement)

Equations

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

theorem Chapter11.BoundedInterval.le_max {I : BoundedInterval} (P P' : Partition I) : P ≤ P ⊔ P' ∧ P' ≤ P ⊔ P'

Лема 11.1.8 / Вправа 11.1.4

theorem Chapter11.BoundedInterval.max_le_iff (I : BoundedInterval) {P P' P'' : Partition I} {hP : P ≤ P''} {hP' : P' ≤ P''} : P ⊔ P' ≤ P''

Not from textbook: the reverse inclusion