Skip to content

Commit c71f075

Browse files
aodecipheraodecipher
committed
Merge remote-tracking branch 'origin/main'
2 parents 968d326 + b42731f commit c71f075

File tree

3 files changed

+352
-1
lines changed

3 files changed

+352
-1
lines changed

‎analysis/Analysis/MeasureTheory/Section_1_4_2.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,8 @@ def MeasurableSpace.toConcreteSigmaAlgebra {X: Type*} (M: MeasurableSpace X) : C
1919

2020
def ConcreteBooleanAlgebra.isSigmaAlgebra {X: Type*} (B: ConcreteBooleanAlgebra X) : Prop := ∀ E : ℕ → Set X, (∀ n, measurable (E n)) → measurable (⋃ n, E n)
2121

22+
theorem ConcreteSigmaAlgebra.isSigmaAlgebra {X: Type*} (B: ConcreteSigmaAlgebra X) : B.isSigmaAlgebra := by sorry
23+
2224
def ConcreteBooleanAlgebra.isSigmaAlgebra.toSigmaAlgebra {X: Type*} {B: ConcreteBooleanAlgebra X} (h: B.isSigmaAlgebra) : ConcreteSigmaAlgebra X :=
2325
{ countable_union_mem := h }
2426

@@ -207,3 +209,20 @@ example (d₁ d₂ :ℕ) (E : Set (EuclideanSpace' (d₁+d₂)))
207209
theorem LebesgueMeasurable.sigmaAlgebra_generated_by {d:ℕ} :
208210
LebesgueMeasurable.sigmaAlgebra d = ConcreteSigmaAlgebra.generated_by ( (BorelSigmaAlgebra (EuclideanSpace' d)).measurableSets ∪ (IsNull.sigmaAlgebra d).measurableSets) :=
209211
by sorry
212+
213+
def ConcreteSigmaAlgebra.measurableSpace {X: Type*} (B: ConcreteSigmaAlgebra X) : MeasurableSpace X := {
214+
MeasurableSet' := B.measurable
215+
measurableSet_empty := B.empty_mem
216+
measurableSet_compl := B.compl_mem
217+
measurableSet_iUnion := B.countable_union_mem
218+
}
219+
220+
def MeasurableSpace.sigmaAlgebra {X: Type*} (M: MeasurableSpace X) : ConcreteSigmaAlgebra X := {
221+
measurable := M.MeasurableSet'
222+
empty_mem := M.measurableSet_empty
223+
compl_mem := M.measurableSet_compl
224+
union_mem := sorry
225+
countable_union_mem := M.measurableSet_iUnion
226+
}
227+
228+
theorem BorelSigmaAlgebra.le_LebesgueSigmaAlgebra (d:ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) ≤ LebesgueMeasurable.sigmaAlgebra d := by sorry

‎analysis/Analysis/MeasureTheory/Section_1_4_3.lean‎

Lines changed: 332 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,336 @@ import Analysis.MeasureTheory.Section_1_4_2
55
66
A companion to (the introduction to) Section 1.4.3 of the book "An introduction to Measure Theory".
77
8+
Note: initially this section will use custom-notions of concrete sigma algebras and countably additive measures, but will transition to the Mathlib notions of `Measurable` and `Measure`, which will be in use going forward. In particular, exercises past this point will be easier
9+
to solve using the Mathlib library for measure theory than the custom results defined here.
810
-/
11+
12+
/-- Definition 1.4.19 (Finitely additive measure) -/
13+
class FinitelyAdditiveMeasure {X:Type*} (B: ConcreteBooleanAlgebra X) where
14+
measure : Set X → EReal
15+
measure_pos : ∀ A : Set X, B.measurable A → 0 ≤ measure A
16+
measure_empty : measure ∅ = 0
17+
measure_finite_additive : ∀ E F : Set X, B.measurable E → B.measurable F → Disjoint E F →
18+
measure (E ∪ F) = measure E + measure F
19+
20+
/-- Example 1.4.21 -/
21+
noncomputable def FinitelyAdditiveMeasure.lebesgue (d:ℕ) : FinitelyAdditiveMeasure (LebesgueMeasurable.boolean_algebra d) :=
22+
{
23+
measure A := Lebesgue_measure A
24+
measure_pos := by sorry
25+
measure_empty := by sorry
26+
measure_finite_additive := by sorry
27+
}
28+
29+
/-- Example 1.4.21 -/
30+
def FinitelyAdditiveMeasure.restrict_alg {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) {B':ConcreteBooleanAlgebra X} (hBB': B' ≤ B) : FinitelyAdditiveMeasure B' :=
31+
{
32+
measure := μ.measure
33+
measure_pos := by sorry
34+
measure_empty := by sorry
35+
measure_finite_additive := by sorry
36+
}
37+
38+
/-- Example 1.4.21 -/
39+
noncomputable def FinitelyAdditiveMeasure.jordan (d:ℕ) : FinitelyAdditiveMeasure (JordanMeasurable.boolean_algebra d) :=
40+
(FinitelyAdditiveMeasure.lebesgue d).restrict_alg (LebesgueMeasurable.gt_jordan_boolean_algebra d)
41+
42+
/-- Example 1.4.21 -/
43+
noncomputable def FinitelyAdditiveMeasure.null (d:ℕ) : FinitelyAdditiveMeasure (IsNull.boolean_algebra d) :=
44+
(FinitelyAdditiveMeasure.lebesgue d).restrict_alg (IsNull.lt_lebesgue_boolean_algebra d)
45+
46+
/-- Example 1.4.21 -/
47+
noncomputable def FinitelyAdditiveMeasure.elem (d:ℕ) : FinitelyAdditiveMeasure (EuclideanSpace'.elementary_boolean_algebra d) :=
48+
(FinitelyAdditiveMeasure.lebesgue d).restrict_alg (by sorry)
49+
50+
open Classical in
51+
/-- Example 1.4.22 (Dirac measure) -/
52+
noncomputable def FinitelyAdditiveMeasure.dirac {X:Type*} (x₀:X) (B: ConcreteBooleanAlgebra X) : FinitelyAdditiveMeasure B :=
53+
{
54+
measure := fun A => if x₀ ∈ A then 1 else 0
55+
measure_pos := by sorry
56+
measure_empty := by sorry
57+
measure_finite_additive := by sorry
58+
}
59+
60+
/-- Example 1.4.23 (Zero measure) -/
61+
instance FinitelyAdditiveMeasure.instZero {X:Type*} (B: ConcreteBooleanAlgebra X) : Zero (FinitelyAdditiveMeasure B) :=
62+
{
63+
zero := {
64+
measure := fun A => 0
65+
measure_pos := by sorry
66+
measure_empty := by sorry
67+
measure_finite_additive := by sorry
68+
}
69+
}
70+
71+
/-- Example 1.4.24 (linear combinations of measures) -/
72+
instance FinitelyAdditiveMeasure.instAdd {X:Type*} {B: ConcreteBooleanAlgebra X} : Add (FinitelyAdditiveMeasure B) :=
73+
{
74+
add := fun μ ν =>
75+
{
76+
measure := fun A => μ.measure A + ν.measure A
77+
measure_pos := by sorry
78+
measure_empty := by sorry
79+
measure_finite_additive := by sorry
80+
}
81+
}
82+
83+
noncomputable instance FinitelyAdditiveMeasure.instSmul {X:Type*} {B: ConcreteBooleanAlgebra X} : SMul ENNReal (FinitelyAdditiveMeasure B) :=
84+
{
85+
smul := fun c μ =>
86+
{
87+
measure := fun A => c * μ.measure A
88+
measure_pos := by sorry
89+
measure_empty := by sorry
90+
measure_finite_additive := by sorry
91+
}
92+
}
93+
94+
instance FinitelyAdditiveMeasure.instAddCommMonoid {X:Type*} {B: ConcreteBooleanAlgebra X} : AddCommMonoid (FinitelyAdditiveMeasure B) :=
95+
{
96+
add_assoc := by sorry,
97+
zero_add := by sorry,
98+
add_zero := by sorry,
99+
add_comm := by sorry
100+
nsmul := nsmulRec
101+
}
102+
103+
noncomputable instance FinitelyAdditiveMeasure.instDistribMulAction {X:Type*} {B: ConcreteBooleanAlgebra X} : DistribMulAction ENNReal (FinitelyAdditiveMeasure B) :=
104+
{
105+
smul_zero := by sorry,
106+
smul_add := by sorry,
107+
one_smul := by sorry,
108+
mul_smul := by sorry
109+
}
110+
111+
/-- Example 1.4.25 (Restriction of a measure) -/
112+
def FinitelyAdditiveMeasure.restrict {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) (A:Set X) (hA:B.measurable A) : FinitelyAdditiveMeasure (B.restrict A) :=
113+
{
114+
measure := fun E => μ.measure E
115+
measure_pos := by sorry
116+
measure_empty := by sorry
117+
measure_finite_additive := by sorry
118+
}
119+
120+
/-- Example 1.4.26 (Counting a measure) -/
121+
noncomputable def FinitelyAdditiveMeasure.counting (X:Type*) : FinitelyAdditiveMeasure (⊤ : ConcreteBooleanAlgebra X) :=
122+
{
123+
measure := fun E => ENat.card E
124+
measure_pos := by sorry
125+
measure_empty := by sorry
126+
measure_finite_additive := by sorry
127+
}
128+
129+
/-- Exercise 1.4.20(i) -/
130+
theorem FinitelyAdditiveMeasure.mono {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) {E F : Set X} (hE : B.measurable E) (hF : B.measurable F) (hsub : E ⊆ F) : μ.measure E ≤ μ.measure F :=
131+
by sorry
132+
133+
/-- Exercise 1.4.20(ii) -/
134+
theorem FinitelyAdditiveMeasure.finite_additivity {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) {J:Type*} {I: Finset J} {E: J → Set X} (hE: ∀ j:J, B.measurable (E j)) (hdisj: Set.univ.PairwiseDisjoint E) :
135+
μ.measure (⋃ j ∈ I, E j) = ∑ j ∈ I, μ.measure (E j) := by sorry
136+
137+
/-- Exercise 1.4.20(iii) -/
138+
theorem FinitelyAdditiveMeasure.finite_subadditivity {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) {J:Type*} {I: Finset J} {E: J → Set X} (hE: ∀ j:J, B.measurable (E j)) :
139+
μ.measure (⋃ j ∈ I, E j) ≤ ∑ j ∈ I, μ.measure (E j) := by sorry
140+
141+
/-- Exercise 1.4.20(iv) -/
142+
theorem FinitelyAdditiveMeasure.mes_union_add_mes_inter {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) (E F : Set X) :
143+
μ.measure (E ∪ F) + μ.measure (E ∩ F) = μ.measure E + μ.measure F := by sorry
144+
145+
open Classical in
146+
/-- Exercise 1.4.21 -/
147+
theorem FinitelyAdditiveMeasure.finite_atomic_eq {I X: Type*} [Fintype I] {atoms: I → Set X} (h_part: IsPartition atoms) (μ : FinitelyAdditiveMeasure h_part.to_ConcreteBooleanAlgebra) : ∃! c : I → ENNReal, ∀ E, h_part.to_ConcreteBooleanAlgebra.measurable E → μ.measure E = ∑ i ∈ Finset.univ.filter (fun i => atoms i ⊆ E), c i := by sorry
148+
149+
/-- Definition 1.4.27 (Countably additive measure) -/
150+
class CountablyAdditiveMeasure {X:Type*} (B: ConcreteSigmaAlgebra X) extends FinitelyAdditiveMeasure B.toConcreteBooleanAlgebra where
151+
measure_countable_additive : ∀ (E : ℕ → Set X), (∀ n, B.measurable (E n)) → Set.univ.PairwiseDisjoint E →
152+
measure (⋃ n, E n) = ∑' n, (measure (E n))
153+
154+
def FinitelyAdditiveMeasure.isCountablyAdditive {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) : Prop :=
155+
B.isSigmaAlgebra ∧ ∀ (E : ℕ → Set X), (∀ n, B.measurable (E n)) → Set.univ.PairwiseDisjoint E →
156+
μ.measure (⋃ n, E n) = ∑' n, (μ.measure (E n))
157+
158+
def FinitelyAdditiveMeasure.isCountablyAdditive.toCountablyAdditive {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: FinitelyAdditiveMeasure B) (h: μ.isCountablyAdditive) : CountablyAdditiveMeasure h.1.toSigmaAlgebra :=
159+
{
160+
measure := μ.measure
161+
measure_pos := μ.measure_pos
162+
measure_empty := μ.measure_empty
163+
measure_finite_additive := μ.measure_finite_additive
164+
measure_countable_additive := h.2
165+
}
166+
167+
/-- Example 1.4.28-/
168+
theorem FinitelyAdditiveMeasure.lebesgue_isCountablyAdditive (d:ℕ) : (FinitelyAdditiveMeasure.lebesgue d).isCountablyAdditive :=
169+
by sorry
170+
171+
theorem FinitelyAdditiveMeasure.isCountablyAdditive_restrict_alg {X:Type*} {B B': ConcreteSigmaAlgebra X} (μ: CountablyAdditiveMeasure B) (hBB': B' ≤ B) : (μ.toFinitelyAdditiveMeasure.restrict_alg hBB').isCountablyAdditive :=
172+
by sorry
173+
174+
def CountablyAdditiveMeasure.restrict_alg {X:Type*} {B B': ConcreteSigmaAlgebra X} (μ: CountablyAdditiveMeasure B) (hBB' : B' ≤ B) : CountablyAdditiveMeasure B' :=
175+
{
176+
toFinitelyAdditiveMeasure := μ.toFinitelyAdditiveMeasure.restrict_alg hBB',
177+
measure_countable_additive := by sorry
178+
}
179+
180+
/-- Example 1.4.29-/
181+
theorem FinitelyAdditiveMeasure.dirac_isCountablyAdditive {X:Type*} (x₀:X) (B: ConcreteBooleanAlgebra X) : (FinitelyAdditiveMeasure.dirac x₀ B).isCountablyAdditive :=
182+
by sorry
183+
184+
/-- Example 1.4.29-/
185+
theorem FinitelyAdditiveMeasure.counting_isCountablyAdditive {X:Type*} : (FinitelyAdditiveMeasure.counting X).isCountablyAdditive :=
186+
by sorry
187+
188+
/-- Example 1.4.30 -/
189+
def CountablyAdditiveMeasure.restrict {X:Type*} {B: ConcreteSigmaAlgebra X} (μ: CountablyAdditiveMeasure B) (A:Set X) (hA:B.measurable A) : CountablyAdditiveMeasure (B.restrict A) :=
190+
{
191+
toFinitelyAdditiveMeasure := μ.toFinitelyAdditiveMeasure.restrict A hA,
192+
measure_countable_additive := by sorry
193+
}
194+
195+
instance CountablyAdditiveMeasure.instZero {X:Type*} (B: ConcreteSigmaAlgebra X) : Zero (CountablyAdditiveMeasure B) :=
196+
{
197+
zero := {
198+
toFinitelyAdditiveMeasure := 0
199+
measure_countable_additive := by sorry
200+
}
201+
}
202+
203+
instance CountablyAdditiveMeasure.instAdd {X:Type*} {B: ConcreteSigmaAlgebra X} : Add (CountablyAdditiveMeasure B) :=
204+
{
205+
add := fun μ ν =>
206+
{
207+
toFinitelyAdditiveMeasure := μ.toFinitelyAdditiveMeasure + ν.toFinitelyAdditiveMeasure
208+
measure_countable_additive := by sorry
209+
}
210+
}
211+
212+
instance CountablyAdditiveMeasure.instAddCommMonoid {X:Type*} {B: ConcreteSigmaAlgebra X} : AddCommMonoid (CountablyAdditiveMeasure B) :=
213+
{
214+
add_assoc := by sorry,
215+
zero_add := by sorry,
216+
add_zero := by sorry,
217+
add_comm := by sorry
218+
nsmul := nsmulRec
219+
}
220+
221+
/-- Exercise 1.4.22(i) -/
222+
noncomputable instance CountablyAdditiveMeasure.instSmul {X:Type*} {B: ConcreteSigmaAlgebra X} : SMul ENNReal (CountablyAdditiveMeasure B) :=
223+
{
224+
smul := fun c μ =>
225+
{
226+
toFinitelyAdditiveMeasure := c • μ.toFinitelyAdditiveMeasure
227+
measure_countable_additive := by sorry
228+
}
229+
}
230+
231+
noncomputable instance CountablyAdditiveMeasure.instDistribMulAction {X:Type*} {B: ConcreteSigmaAlgebra X} : DistribMulAction ENNReal (CountablyAdditiveMeasure B) :=
232+
{
233+
smul_zero := by sorry,
234+
smul_add := by sorry,
235+
one_smul := by sorry,
236+
mul_smul := by sorry
237+
}
238+
239+
/-- Exercise 1.4.22(ii) -/
240+
noncomputable def CountablyAdditiveMeasure.sum {X:Type*} {B: ConcreteSigmaAlgebra X} (μ: ℕ → CountablyAdditiveMeasure B) : CountablyAdditiveMeasure B :=
241+
{
242+
toFinitelyAdditiveMeasure := {
243+
measure := fun A => ∑' n, (μ n).toFinitelyAdditiveMeasure.measure A
244+
measure_pos := by sorry
245+
measure_empty := by sorry
246+
measure_finite_additive := by sorry
247+
}
248+
measure_countable_additive := by sorry
249+
}
250+
251+
open MeasureTheory
252+
253+
noncomputable def CountablyAdditiveMeasure.toMeasure {X:Type*} {B: ConcreteSigmaAlgebra X} (μ: CountablyAdditiveMeasure B) :
254+
@Measure X B.measurableSpace :=
255+
let _measurable := B.measurableSpace
256+
{
257+
measureOf E := (μ.measure E).toENNReal
258+
empty := by sorry
259+
mono := by sorry
260+
iUnion_nat := by sorry
261+
m_iUnion := by sorry
262+
trim_le := by sorry
263+
}
264+
265+
noncomputable def FinitelyAdditiveMeasure.isCountablyAdditive.toMeasure {X:Type*} {B: ConcreteBooleanAlgebra X} {μ: FinitelyAdditiveMeasure B} (h: μ.isCountablyAdditive) :
266+
@Measure X h.1.toSigmaAlgebra.measurableSpace := h.toCountablyAdditive.toMeasure
267+
268+
def Measure.toCountablyAdditiveMeasure {X:Type*} [M : MeasurableSpace X] (μ: Measure X) : CountablyAdditiveMeasure M.sigmaAlgebra :=
269+
{
270+
toFinitelyAdditiveMeasure := {
271+
measure E := μ.measureOf E
272+
measure_pos := by sorry
273+
measure_empty := by sorry
274+
measure_finite_additive := by sorry
275+
}
276+
measure_countable_additive := by sorry
277+
}
278+
279+
/-- Exercise 1.4.23(i) -/
280+
theorem Measure.countable_subadditivity {X:Type*} [MeasurableSpace X] (μ: Measure X) {E : ℕ → Set X} (hE: ∀ n, Measurable (E n)) :
281+
μ.measureOf (⋃ n, E n) ≤ ∑' n, μ.measureOf (E n) := by sorry
282+
283+
/-- Exercise 1.4.23(ii) -/
284+
theorem Measure.upwards_mono {X:Type*} [MeasurableSpace X] (μ: Measure X) {E : ℕ → Set X} (hE: ∀ n, Measurable (E n))
285+
(hmono : Monotone E) : μ (⋃ n, E n) = ⨆ n, μ.measureOf (E n) := by sorry
286+
287+
/-- Exercise 1.4.23(iii) -/
288+
theorem Measure.downwards_mono {X:Type*} [MeasurableSpace X] (μ: Measure X) {E : ℕ → Set X} (hE: ∀ n, Measurable (E n))
289+
(hmono : Antitone E) (hfin : ∃ n, μ (E n) < ⊤) : μ (⋂ n, E n) = ⨅ n, μ.measureOf (E n) := by sorry
290+
291+
theorem Measure.downwards_mono_counter : ∃ (X:Type) (M: MeasurableSpace X) (μ: Measure X) (E : ℕ → Set X) (hE: ∀ n, Measurable (E n))
292+
(hmono : Antitone E), μ (⋂ n, E n) ≠ ⨅ n, μ.measureOf (E n) := by sorry
293+
294+
/-- Exercise 1.4.24 (i) (Dominated convergence for sets) -/
295+
theorem Measure.measurable_of_lim {X:Type*} [MeasurableSpace X] (μ: Measure X) {E : ℕ → Set X} (hE: ∀ n, Measurable (E n))
296+
{E' : Set X} (hlim : PointwiseConvergesTo E E') : Measurable E := by sorry
297+
298+
/-- Exercise 1.4.24 (ii) (Dominated convergence for sets) -/
299+
theorem Measure.measure_of_lim {X:Type*} [MeasurableSpace X] (μ: Measure X) {E : ℕ → Set X} (hE: ∀ n, Measurable (E n))
300+
{E' F : Set X} (hlim : PointwiseConvergesTo E E') (hF : Measurable F) (hfin : μ F < ⊤) (hcon : ∀ n, E n ⊆ F) :
301+
Filter.atTop.Tendsto (fun n ↦ μ (E n)) (nhds (μ E')) := by sorry
302+
303+
/-- Exercise 1.4.24 (iii) (Dominated convergence for sets) -/
304+
theorem Measure.measure_of_lim_counter : ∃ (X:Type) (M:MeasurableSpace X) (μ: Measure X) (E : ℕ → Set X) (hE: ∀ n, Measurable (E n))
305+
(E' F : Set X) (hlim : PointwiseConvergesTo E E') (hF : Measurable F) (hcon : ∀ n, E n ⊆ F),
306+
¬ Filter.atTop.Tendsto (fun n ↦ μ (E n)) (nhds (μ E')) := by sorry
307+
308+
/-- Exercise 1.4.25 -/
309+
theorem Measure.on_countable {X:Type*} [Countable X] [M: MeasurableSpace X] (hM: M = ⊤) (μ: Measure X) :
310+
∃! c : X → ENNReal, ∀ E : Set X, μ E = ∑' x : E, c x := by sorry
311+
312+
-- Definition 1.4.31
313+
#check Measure.IsComplete
314+
315+
#check NullMeasurableSpace
316+
317+
#check Measure.completion
318+
319+
/-- Exercise 1.4.26 (Completion) -/
320+
theorem Measure.completion_lt {X:Type*} [M : MeasurableSpace X] (μ: Measure X) (M' : MeasurableSpace X) (μ' : @Measure X M')
321+
(hMM' : M ≤ M') (hμ : ∀ E, M.MeasurableSet' E → μ E = μ' E) : ∀ E : Set X, @NullMeasurableSet X M E μ → (M'.MeasurableSet' E ∧ μ' E = μ.completion E)
322+
:= by sorry
323+
324+
noncomputable def EuclideanSpace'.lebesgueMeasure (d:ℕ) := (FinitelyAdditiveMeasure.lebesgue_isCountablyAdditive d).toMeasure
325+
326+
noncomputable def EuclideanSpace'.borelMeasure (d:ℕ) := ((FinitelyAdditiveMeasure.lebesgue_isCountablyAdditive d).toCountablyAdditive.restrict_alg (BorelSigmaAlgebra.le_LebesgueSigmaAlgebra d)).toMeasure
327+
328+
def Measure.equiv {X:Type*} {M M' : MeasurableSpace X} (μ: @Measure X M) (μ': @Measure X M') : Prop := M = M' ∧ ∀ E, M.MeasurableSet' E → μ E = μ' E
329+
330+
/-- Exercise 1.4.27 -/
331+
theorem EuclideanSpace'.borel_completion_eq_lebesgue {d:ℕ} :
332+
Measure.equiv (EuclideanSpace'.borelMeasure d).completion (EuclideanSpace'.lebesgueMeasure d) := by sorry
333+
334+
/-- Exercise 1.4.28(i) (Approximation by an algebra) -/
335+
theorem BooleanAlgebra.approx_finite {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: @Measure X (ConcreteSigmaAlgebra.generated_by B.measurableSets).measurableSpace) (hfin: μ Set.univ < ⊤) : ∀ (ε : ℝ) (hε: ε>0) (E : Set X) (hE: (ConcreteSigmaAlgebra.generated_by B.measurableSets).measurable E),
336+
∃ F : Set X, B.measurable F ∧ μ (symmDiff E F) < ENNReal.ofReal ε := by sorry
337+
338+
/-- Exercise 1.4.28(ii) (Approximation by an algebra) -/
339+
theorem BooleanAlgebra.approx_sigma_finite {X:Type*} {B: ConcreteBooleanAlgebra X} (μ: @Measure X (ConcreteSigmaAlgebra.generated_by B.measurableSets).measurableSpace) (hσfin: ∃ A : ℕ → Set X, (∀ n, B.measurable (A n) ∧ μ (A n) < ⊤) ∧ ⋃ n, A n = ⊤) : ∀ (ε : ℝ) (hε: ε>0) (E : Set X) (hE: (ConcreteSigmaAlgebra.generated_by B.measurableSets).measurable E),
340+
∃ F : Set X, B.measurable F ∧ μ (symmDiff E F) < ENNReal.ofReal ε := by sorry

‎analysis/Analysis/Section_9_6.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ example : ¬ BddOn (fun x:ℝ ↦ 1/x) (.Ioo 0 1) := by sorry
4747

4848
theorem why_7_6_3 {n: ℕ → ℕ} (hn: StrictMono n) (j:ℕ) : n j ≥ j := by sorry
4949

50-
/-- Lemma 7.6.3 -/
50+
/-- Lemma 9.6.3 -/
5151
theorem BddOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b) ) :
5252
BddOn f (.Icc a b) := by
5353
-- This proof is written to follow the structure of the original text.

0 commit comments

Comments
 (0)