Documentation

Analysis.Section_11_1

Analysis I, Section 11.1: Partitions #

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 :

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

Instances For

def Chapter11.BoundedInterval.toSet (I : BoundedInterval) :

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

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

Instances For

instance Chapter11.BoundedInterval.inst_coeSet :

Coe BoundedInterval (Set ℝ)

Equations

Chapter11.BoundedInterval.inst_coeSet = { coe := Chapter11.BoundedInterval.toSet }

instance Chapter11.BoundedInterval.instEmpty :

EmptyCollection BoundedInterval

Equations

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

@[simp]

theorem Chapter11.BoundedInterval.coe_empty :

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 : ℝ) :

↑(Ioo a b) = Set.Ioo a b

@[simp]

theorem Chapter11.BoundedInterval.set_Icc (a b : ℝ) :

↑(Icc a b) = Set.Icc a b

@[simp]

theorem Chapter11.BoundedInterval.set_Ioc (a b : ℝ) :

↑(Ioc a b) = Set.Ioc a b

@[simp]

theorem Chapter11.BoundedInterval.set_Ico (a b : ℝ) :

↑(Ico a b) = Set.Ico a b

theorem Chapter11.Bornology.IsBounded.of_boundedInterval (I : BoundedInterval) :

Bornology.IsBounded ↑I

Lemma 11.1.4 / Exercise 11.1.1

theorem Chapter11.BoundedInterval.ordConnected_iff (X : Set ℝ) :

Bornology.IsBounded X ∧ X.OrdConnected ↔ ∃ (I : BoundedInterval), X = ↑I

theorem Chapter11.BoundedInterval.inter (I J : BoundedInterval) :

∃ (K : BoundedInterval), ↑I ∩ ↑J = ↑K

Corollary 11.1.6 / Exercise 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) :

↑(I ∩ J) = ↑I ∩ ↑J

instance Chapter11.BoundedInterval.instMembership :

Membership ℝ BoundedInterval

Equations

Chapter11.BoundedInterval.instMembership = { mem := fun (I : Chapter11.BoundedInterval) (x : ℝ) => x ∈ ↑I }

theorem Chapter11.BoundedInterval.mem_iff (I : BoundedInterval) (x : ℝ) :

x ∈ I ↔ x ∈ ↑I

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 ↔ ↑I ⊆ ↑J

@[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

Instances For

@[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

Instances For

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

Instances For

def Chapter11.«term|___|ₗ» :

Lean.ParserDescr

Using ||ₗ subscript here to not override ||

Equations

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

Instances For

theorem Chapter11.BoundedInterval.length_nonneg (I : BoundedInterval) :

theorem Chapter11.BoundedInterval.empty_of_lt {I : BoundedInterval} (h : I.b < I.a) :

↑I = ∅

theorem Chapter11.BoundedInterval.length_of_empty {I : BoundedInterval} (hI : ↑I = ∅) :

theorem Chapter11.BoundedInterval.length_of_subsingleton {I : BoundedInterval} :

Subsingleton ↑↑I ↔ I.length = 0

theorem Chapter11.BoundedInterval.dist_le_length {I : BoundedInterval} {x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) :

|x - y| ≤ I.length

@[reducible, inline]

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

Equations

K.joins I J = (↑I ∩ ↑J = ∅ ∧ ↑K = ↑I ∪ ↑J ∧ K.length = I.length + J.length)

Instances For

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

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

Instances For

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

Equations

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

Instances For

@[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) :

Equations

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

Instances For

@[reducible, inline]

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

Equations

P.remove_empty = { intervals := {J ∈ P.intervals | (↑J).Nonempty}, exists_unique := ⋯, contains := ⋯ }

Instances For

@[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

Exercise 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

Theorem 11.1.13 (Length is finitely additive).

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

LE (Partition I)

Definition 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_ge := ⋯ }

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)

Definition 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'

Lemma 11.1.8 / Exercise 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