Skip to content

Commit 7ea5f3f

Browse files
teorthteorth
authored
Merge pull request #292 from teorth:json-revert
attempting to revert json
2 parents 16d5097 + d1608cb commit 7ea5f3f

5 files changed

Lines changed: 287 additions & 17 deletions

File tree

‎analysis/Analysis/MeasureTheory/Notation.lean‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -171,4 +171,17 @@ theorem ENNReal.tsum_of_tsum' (x: ℕ → ℕ → ENNReal) : ∑' p:ℕ × ℕ,
171171

172172
#check ENNReal.tsum_comm
173173

174-
/-- Exercise 0.0.2 -/
174+
/-- Exercise 0.0.2 (Tonelli's theorem for series over arbitrary sets)-/
175+
example {A B:Type*} (x: A → B → ENNReal) : ∑' p:A × B, x p.1 p.2 = ∑' a, ∑' b, x a b := by
176+
sorry
177+
178+
example {A B:Type*} (x: A → B → ENNReal) : ∑' p:A × B, x p.1 p.2 = ∑' b, ∑' a, x a b := by
179+
sorry
180+
181+
/-- Axiom 0.0.4 (Axiom of choice)-/
182+
noncomputable def Set.choose {A: Type*} {E: A → Type*} (hE: ∀ n, Nonempty (E n)) :
183+
∀ n, E n := fun n ↦ (hE n).some
184+
185+
/-- Corollary 0.0.5 (Axiom of countable choice) -/
186+
noncomputable def Countable.choose {E: ℕ → Type*} (hE: ∀ n, Nonempty (E n)) :
187+
∀ n, E n := Set.choose hE

‎analysis/Analysis/MeasureTheory/Section_1_1_1.lean‎

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
import Analysis.MeasureTheory.Notation
2+
3+
/-!
4+
# Introduction to Measure Theory, Section 1.1.1: Elementary measure
5+
6+
A companion to Section 1.1.1 of the book "An introduction to Measure Theory".
7+
8+
-/
9+
10+
/- Definition 1.1.1. (Intervals) We use the same formalization of intervals used in
11+
Chapter 11 of "Analysis I". Following the usual Lean preference to admit `junk` values,
12+
we allow for the possibility that `b < a`. -/
13+
inductive BoundedInterval where
14+
| Ioo (a b:ℝ) : BoundedInterval
15+
| Icc (a b:ℝ) : BoundedInterval
16+
| Ioc (a b:ℝ) : BoundedInterval
17+
| Ico (a b:ℝ) : BoundedInterval
18+
19+
open BoundedInterval
20+
21+
@[coe]
22+
def BoundedInterval.toSet (I: BoundedInterval) : Set ℝ := match I with
23+
| Ioo a b => .Ioo a b
24+
| Icc a b => .Icc a b
25+
| Ioc a b => .Ioc a b
26+
| Ico a b => .Ico a b
27+
28+
instance BoundedInterval.inst_coeSet : Coe BoundedInterval (Set ℝ) where
29+
coe := toSet
30+
31+
instance BoundedInterval.instEmpty : EmptyCollection BoundedInterval where
32+
emptyCollection := Ioo 0 0
33+
34+
@[simp]
35+
theorem BoundedInterval.coe_empty : ((∅ : BoundedInterval):Set ℝ) = ∅ := by
36+
simp [toSet]
37+
38+
open Classical in
39+
/-- This is to make Finsets of BoundedIntervals work properly -/
40+
noncomputable instance BoundedInterval.decidableEq : DecidableEq BoundedInterval := instDecidableEqOfLawfulBEq
41+
42+
@[simp]
43+
theorem BoundedInterval.set_Ioo (a b:ℝ) : (Ioo a b : Set ℝ) = .Ioo a b := by rfl
44+
45+
@[simp]
46+
theorem BoundedInterval.set_Icc (a b:ℝ) : (Icc a b : Set ℝ) = .Icc a b := by rfl
47+
48+
@[simp]
49+
theorem BoundedInterval.set_Ioc (a b:ℝ) : (Ioc a b : Set ℝ) = .Ioc a b := by rfl
50+
51+
@[simp]
52+
theorem BoundedInterval.set_Ico (a b:ℝ) : (Ico a b : Set ℝ) = .Ico a b := by rfl
53+
54+
/-- Some helpful general lemmas about BoundedInterval -/
55+
theorem Bornology.IsBounded.of_boundedInterval (I: BoundedInterval) : Bornology.IsBounded (I:Set ℝ) := by
56+
sorry
57+
58+
theorem BoundedInterval.ordConnected_iff (X:Set ℝ) : Bornology.IsBounded X ∧ X.OrdConnected ↔ ∃ I: BoundedInterval, X = I := by
59+
sorry
60+
61+
theorem BoundedInterval.inter (I J: BoundedInterval) : ∃ K : BoundedInterval, (I:Set ℝ) ∩ (J:Set ℝ) = (K:Set ℝ) := by
62+
sorry
63+
64+
noncomputable instance BoundedInterval.instInter : Inter BoundedInterval where
65+
inter I J := (inter I J).choose
66+
67+
@[simp]
68+
theorem BoundedInterval.inter_eq (I J: BoundedInterval) : (I ∩ J : BoundedInterval) = (I:Set ℝ) ∩ (J:Set ℝ) :=
69+
(inter I J).choose_spec.symm
70+
71+
instance BoundedInterval.instMembership : Membership ℝ BoundedInterval where
72+
mem I x := x ∈ (I:Set ℝ)
73+
74+
theorem BoundedInterval.mem_iff (I: BoundedInterval) (x:ℝ) :
75+
x ∈ I ↔ x ∈ (I:Set ℝ) := by rfl
76+
77+
instance BoundedInterval.instSubset : HasSubset BoundedInterval where
78+
Subset I J := ∀ x, x ∈ I → x ∈ J
79+
80+
theorem BoundedInterval.subset_iff (I J: BoundedInterval) :
81+
I ⊆ J ↔ (I:Set ℝ) ⊆ (J:Set ℝ) := by rfl
82+
83+
abbrev BoundedInterval.a (I: BoundedInterval) : ℝ := match I with
84+
| Ioo a _ => a
85+
| Icc a _ => a
86+
| Ioc a _ => a
87+
| Ico a _ => a
88+
89+
abbrev BoundedInterval.b (I: BoundedInterval) : ℝ := match I with
90+
| Ioo _ b => b
91+
| Icc _ b => b
92+
| Ioc _ b => b
93+
| Ico _ b => b
94+
95+
/-- Definition 1.1.1 (boxes) -/
96+
abbrev BoundedInterval.length (I: BoundedInterval) : ℝ := max (I.b - I.a) 0
97+
98+
/-- Using ||ₗ subscript here to not override || -/
99+
macro:max atomic("|" noWs) a:term noWs "|ₗ" : term => `(BoundedInterval.length $a)
100+
101+
@[ext]
102+
structure Box (d:ℕ) where
103+
side : Fin d → BoundedInterval
104+
105+
@[coe]
106+
abbrev Box.toSet {d:ℕ} (B: Box d) : Set (EuclideanSpace' d) :=
107+
Set.univ.pi (fun i ↦ ↑(B.side i))
108+
109+
instance Box.inst_coeSet {d:ℕ} : Coe (Box d) (Set (EuclideanSpace' d)) where
110+
coe := toSet
111+
112+
/-- Definition 1.1.1 (boxes)-/
113+
abbrev Box.volume {d:ℕ} (B: Box d) : ℝ := ∏ i, |B.side i|ₗ
114+
115+
/-- Using ||ᵥ subscript here to not override || -/
116+
macro:max atomic("|" noWs) a:term noWs "|ᵥ" : term => `(Box.volume $a)
117+
118+
abbrev IsElementary {d:ℕ} (E: Set (EuclideanSpace' d)) : Prop := ∃ S : Finset (Box d), E = ⋃ B ∈ S, ↑B
119+
120+
/-- Exercise 1.1.1 (Boolean closure) -/
121+
theorem IsElementary.union {d:ℕ} {E F: Set (EuclideanSpace' d)}
122+
(hE: IsElementary E) (hF: IsElementary F) : IsElementary (E ∪ F) := by
123+
sorry
124+
125+
/-- Exercise 1.1.1 (Boolean closure) -/
126+
theorem IsElementary.inter {d:ℕ} {E F: Set (EuclideanSpace' d)}
127+
(hE: IsElementary E) (hF: IsElementary F) : IsElementary (E ∩ F) := by
128+
sorry
129+
130+
131+
/-- Exercise 1.1.1 (Boolean closure) -/
132+
theorem IsElementary.sdiff {d:ℕ} {E F: Set (EuclideanSpace' d)}
133+
(hE: IsElementary E) (hF: IsElementary F) : IsElementary (E \ F) := by
134+
sorry
135+
136+
/-- Exercise 1.1.1 (Boolean closure) -/
137+
theorem IsElementary.symmDiff {d:ℕ} {E F: Set (EuclideanSpace' d)}
138+
(hE: IsElementary E) (hF: IsElementary F) : IsElementary (symmDiff E F) := by
139+
sorry
140+
141+
open Pointwise
142+
143+
/-- Exercise 1.1.1 (Boolean closure) -/
144+
theorem IsElementary.translate {d:ℕ} {E: Set (EuclideanSpace' d)}
145+
(hE: IsElementary E) (x: EuclideanSpace' d) : IsElementary (E + {x}) := by
146+
sorry
147+

‎analysis/Analysis/Section_11_1.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ noncomputable instance BoundedInterval.instInter : Inter BoundedInterval where
9090

9191
@[simp]
9292
theorem BoundedInterval.inter_eq (I J: BoundedInterval) : (I ∩ J : BoundedInterval) = (I:Set ℝ) ∩ (J:Set ℝ) :=
93-
(BoundedInterval.inter I J).choose_spec.symm
93+
(inter I J).choose_spec.symm
9494

9595
example :
9696
(Ioo 2 4 ∩ Icc 4 6) = (Icc 4 4 : Set ℝ) := by

‎analysis/lake-manifest.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
18+
"rev": "feac4e0c356b0928657bf3b54fa83ae952f53257",
1919
"name": "MD4Lean",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "ffe97dbb0002e15acd571649e93cecfb3d7c47d5",
28+
"rev": "bbbf8ea29a2a80a04c157d4fd8a8997f804569a5",
2929
"name": "subverso",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",

‎book/lake-manifest.json‎

Lines changed: 123 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,145 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url": "https://github.com/leanprover/subverso.git",
4+
[{"url": "https://github.com/leanprover/doc-gen4",
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "79c973b07e2f43c4ac1cec720bbe20b4fbfbd0e9",
9-
"name": "subverso",
8+
"rev": "6df51fead1a3080290edb27cafd4283f037d0363",
9+
"name": "«doc-gen4»",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "79c973b07e2f43c4ac1cec720bbe20b4fbfbd0e9",
11+
"inputRev": "main",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
14-
{"url": "https://github.com/leanprover/verso.git",
14+
{"url": "https://github.com/acmepjz/md4lean",
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "2f79b236be3f02c0207625cff37cec686d39fa0c",
19-
"name": "verso",
18+
"rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
19+
"name": "MD4Lean",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
2222
"inherited": false,
2323
"configFile": "lakefile.lean"},
24-
{"url": "https://github.com/acmepjz/md4lean",
24+
{"url": "https://github.com/leanprover/subverso.git",
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
29-
"name": "MD4Lean",
28+
"rev": "ffe97dbb0002e15acd571649e93cecfb3d7c47d5",
29+
"name": "subverso",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": false,
33+
"configFile": "lakefile.lean"},
34+
{"url": "https://github.com/leanprover-community/mathlib4.git",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "",
38+
"rev": "5c0c94b3f563ed756b48b9439788c53b0d56a897",
39+
"name": "mathlib",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "v4.20.1",
42+
"inherited": false,
43+
"configFile": "lakefile.lean"},
44+
{"url": "https://github.com/mhuisi/lean4-cli",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "",
48+
"rev": "a0abd472348dd725adbb26732e79b26e7e220913",
49+
"name": "Cli",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "main",
52+
"inherited": true,
53+
"configFile": "lakefile.toml"},
54+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "",
58+
"rev": "9f94839235c03d3e04aaed60d277a287f9c84873",
59+
"name": "UnicodeBasic",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "main",
62+
"inherited": true,
63+
"configFile": "lakefile.lean"},
64+
{"url": "https://github.com/dupuisf/BibtexQuery",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "",
68+
"rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69",
69+
"name": "BibtexQuery",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "master",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/plausible",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "2ac43674e92a695e96caac19f4002b25434636da",
79+
"name": "plausible",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover-community",
88+
"rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
89+
"name": "LeanSearchClient",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"},
94+
{"url": "https://github.com/leanprover-community/import-graph",
95+
"type": "git",
96+
"subDir": null,
97+
"scope": "leanprover-community",
98+
"rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
99+
"name": "importGraph",
100+
"manifestFile": "lake-manifest.json",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.toml"},
104+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
105+
"type": "git",
106+
"subDir": null,
107+
"scope": "leanprover-community",
108+
"rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
109+
"name": "proofwidgets",
110+
"manifestFile": "lake-manifest.json",
111+
"inputRev": "v0.0.60",
112+
"inherited": true,
113+
"configFile": "lakefile.lean"},
114+
{"url": "https://github.com/leanprover-community/aesop",
115+
"type": "git",
116+
"subDir": null,
117+
"scope": "leanprover-community",
118+
"rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
119+
"name": "aesop",
120+
"manifestFile": "lake-manifest.json",
121+
"inputRev": "master",
122+
"inherited": true,
123+
"configFile": "lakefile.toml"},
124+
{"url": "https://github.com/leanprover-community/quote4",
125+
"type": "git",
126+
"subDir": null,
127+
"scope": "leanprover-community",
128+
"rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
129+
"name": "Qq",
130+
"manifestFile": "lake-manifest.json",
131+
"inputRev": "master",
132+
"inherited": true,
133+
"configFile": "lakefile.toml"},
134+
{"url": "https://github.com/leanprover-community/batteries",
135+
"type": "git",
136+
"subDir": null,
137+
"scope": "leanprover-community",
138+
"rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
139+
"name": "batteries",
30140
"manifestFile": "lake-manifest.json",
31141
"inputRev": "main",
32142
"inherited": true,
33-
"configFile": "lakefile.lean"}],
34-
"name": "«analysis-book»",
35-
"lakeDir": ".lake"}
143+
"configFile": "lakefile.toml"}],
144+
"name": "Analysis",
145+
"lakeDir": ".lake"}

0 commit comments

Comments
 (0)