Skip to content

Commit 4836110

Browse files
vihdzpvihdzp
committed
feat(SetTheory/Ordinal/Veblen): the two-arguments Veblen function (#18611)
We define the Veblen function `veblen o a` on ordinals, so that `veblen 0 a = ω ^ a` and `veblen o` enumerates the common fixed points of `veblen o'` for `o' < o`. We then prove some basic properties.
1 parent 19e9024 commit 4836110

File tree

3 files changed

+342
-0
lines changed

3 files changed

+342
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5010,6 +5010,7 @@ import Mathlib.SetTheory.Ordinal.Notation
50105010
import Mathlib.SetTheory.Ordinal.Principal
50115011
import Mathlib.SetTheory.Ordinal.Rank
50125012
import Mathlib.SetTheory.Ordinal.Topology
5013+
import Mathlib.SetTheory.Ordinal.Veblen
50135014
import Mathlib.SetTheory.Surreal.Basic
50145015
import Mathlib.SetTheory.Surreal.Dyadic
50155016
import Mathlib.SetTheory.Surreal.Multiplication

‎Mathlib/SetTheory/Ordinal/FixedPoint.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -163,6 +163,10 @@ theorem isNormal_derivFamily [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.
163163
@[deprecated isNormal_derivFamily (since := "2024-10-11")]
164164
alias derivFamily_isNormal := isNormal_derivFamily
165165

166+
theorem derivFamily_strictMono [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) :
167+
StrictMono (derivFamily f) :=
168+
(isNormal_derivFamily f).strictMono
169+
166170
theorem derivFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (o : Ordinal) :
167171
f i (derivFamily f o) = derivFamily f o := by
168172
induction' o using limitRecOn with o _ o l IH
@@ -538,6 +542,9 @@ theorem isNormal_deriv (f) : IsNormal (deriv f) :=
538542
@[deprecated isNormal_deriv (since := "2024-10-11")]
539543
alias deriv_isNormal := isNormal_deriv
540544

545+
theorem deriv_strictMono (f) : StrictMono (deriv f) :=
546+
derivFamily_strictMono _
547+
541548
theorem deriv_id_of_nfp_id {f : Ordinal → Ordinal} (h : nfp f = id) : deriv f = id :=
542549
((isNormal_deriv _).eq_iff_zero_and_succ IsNormal.refl).2 (by simp [h])
543550

‎Mathlib/SetTheory/Ordinal/Veblen.lean‎

Lines changed: 334 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,334 @@
1+
/-
2+
Copyright (c) 2024 Violeta Hernández Palacios. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Violeta Hernández Palacios
5+
-/
6+
import Mathlib.SetTheory.Ordinal.FixedPoint
7+
8+
/-!
9+
# Veblen hierarchy
10+
11+
We define the two-arguments Veblen function, which satisfies `veblen 0 a = ω ^ a` and that for
12+
`o ≠ 0`, `veblen o` enumerates the common fixed points of `veblen o'` for `o' < o`.
13+
14+
## Main definitions
15+
16+
* `veblenWith`: The Veblen hierarchy with a specified initial function.
17+
* `veblen`: The Veblen hierarchy starting with `ω ^ ·`.
18+
19+
## TODO
20+
21+
- Define the epsilon numbers and gamma numbers.
22+
- Prove that `ε₀` and `Γ₀` are countable.
23+
- Prove that the exponential principal ordinals are the epsilon ordinals (and 0, 1, 2, ω).
24+
- Prove that the ordinals principal under `veblen` are the gamma ordinals (and 0).
25+
-/
26+
27+
noncomputable section
28+
29+
universe u
30+
31+
namespace Ordinal
32+
33+
variable {f : Ordinal.{u} → Ordinal.{u}} {o o₁ o₂ a b : Ordinal.{u}}
34+
35+
/-! ### Veblen function with a given starting function -/
36+
37+
section veblenWith
38+
39+
/-- `veblenWith f o` is the `o`-th function in the Veblen hierarchy starting with `f`. This is
40+
defined so that
41+
42+
- `veblenWith f 0 = f`.
43+
- `veblenWith f o` for `o ≠ 0` enumerates the common fixed points of `veblenWith f o'` over all
44+
`o' < o`.
45+
-/
46+
@[pp_nodot]
47+
def veblenWith (f : Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}) : Ordinal.{u} → Ordinal.{u} :=
48+
if o = 0 then f else derivFamily fun (⟨x, _⟩ : Set.Iio o) ↦ veblenWith f x
49+
termination_by o
50+
51+
@[simp]
52+
theorem veblenWith_zero (f : Ordinal → Ordinal) : veblenWith f 0 = f := by
53+
rw [veblenWith, if_pos rfl]
54+
55+
theorem veblenWith_of_ne_zero (f : Ordinal → Ordinal) (h : o ≠ 0) :
56+
veblenWith f o = derivFamily fun x : Set.Iio o ↦ veblenWith f x.1 := by
57+
rw [veblenWith, if_neg h]
58+
59+
/-- `veblenWith f o` is always normal for `o ≠ 0`. See `isNormal_veblenWith` for a version which
60+
assumes `IsNormal f`. -/
61+
theorem isNormal_veblenWith' (f : Ordinal → Ordinal) (h : o ≠ 0) : IsNormal (veblenWith f o) := by
62+
rw [veblenWith_of_ne_zero f h]
63+
exact isNormal_derivFamily _
64+
65+
variable (hf : IsNormal f)
66+
include hf
67+
68+
/-- `veblenWith f o` is always normal whenever `f` is. See `isNormal_veblenWith'` for a version
69+
which does not assume `IsNormal f`. -/
70+
theorem isNormal_veblenWith (o : Ordinal) : IsNormal (veblenWith f o) := by
71+
obtain rfl | h := eq_or_ne o 0
72+
· rwa [veblenWith_zero]
73+
· exact isNormal_veblenWith' f h
74+
75+
protected alias IsNormal.veblenWith := isNormal_veblenWith
76+
77+
theorem veblenWith_veblenWith_of_lt (h : o₁ < o₂) (a : Ordinal) :
78+
veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a := by
79+
let x : Set.Iio _ := ⟨o₁, h⟩
80+
rw [veblenWith_of_ne_zero f h.bot_lt.ne',
81+
derivFamily_fp (f := fun y : Set.Iio o₂ ↦ veblenWith f y.1) (i := x)]
82+
exact hf.veblenWith x
83+
84+
theorem veblenWith_succ (o : Ordinal) : veblenWith f (Order.succ o) = deriv (veblenWith f o) := by
85+
rw [deriv_eq_enumOrd (hf.veblenWith o), veblenWith_of_ne_zero f (succ_ne_zero _),
86+
derivFamily_eq_enumOrd]
87+
· apply congr_arg
88+
ext a
89+
rw [Set.mem_iInter]
90+
use fun ha ↦ ha ⟨o, Order.lt_succ o⟩
91+
rintro (ha : _ = _) ⟨b, hb : b < _⟩
92+
obtain rfl | hb := Order.lt_succ_iff_eq_or_lt.1 hb
93+
· rw [Function.mem_fixedPoints_iff, ha]
94+
· rw [← ha]
95+
exact veblenWith_veblenWith_of_lt hf hb _
96+
· exact fun o ↦ hf.veblenWith o.1
97+
98+
theorem veblenWith_right_strictMono (o : Ordinal) : StrictMono (veblenWith f o) :=
99+
(hf.veblenWith o).strictMono
100+
101+
@[simp]
102+
theorem veblenWith_lt_veblenWith_iff_right : veblenWith f o a < veblenWith f o b ↔ a < b :=
103+
(veblenWith_right_strictMono hf o).lt_iff_lt
104+
105+
@[simp]
106+
theorem veblenWith_le_veblenWith_iff_right : veblenWith f o a ≤ veblenWith f o b ↔ a ≤ b :=
107+
(veblenWith_right_strictMono hf o).le_iff_le
108+
109+
theorem veblenWith_injective (o : Ordinal) : Function.Injective (veblenWith f o) :=
110+
(veblenWith_right_strictMono hf o).injective
111+
112+
@[simp]
113+
theorem veblenWith_inj : veblenWith f o a = veblenWith f o b ↔ a = b :=
114+
(veblenWith_injective hf o).eq_iff
115+
116+
theorem right_le_veblenWith (o a : Ordinal) : a ≤ veblenWith f o a :=
117+
(veblenWith_right_strictMono hf o).le_apply
118+
119+
theorem veblenWith_left_monotone (a : Ordinal) : Monotone (veblenWith f · a) := by
120+
rw [monotone_iff_forall_lt]
121+
intro o₁ o₂ h
122+
rw [← veblenWith_veblenWith_of_lt hf h]
123+
exact (veblenWith_right_strictMono hf o₁).monotone (right_le_veblenWith hf o₂ a)
124+
125+
theorem veblenWith_pos (hp : 0 < f 0) : 0 < veblenWith f o a := by
126+
have H (b) : 0 < veblenWith f 0 b := by
127+
rw [veblenWith_zero]
128+
exact hp.trans_le (hf.monotone (Ordinal.zero_le _))
129+
obtain rfl | h := Ordinal.eq_zero_or_pos o
130+
· exact H a
131+
· rw [← veblenWith_veblenWith_of_lt hf h]
132+
exact H _
133+
134+
theorem veblenWith_zero_strictMono (hp : 0 < f 0) : StrictMono (veblenWith f · 0) := by
135+
intro o₁ o₂ h
136+
dsimp only
137+
rw [← veblenWith_veblenWith_of_lt hf h, veblenWith_lt_veblenWith_iff_right hf]
138+
exact veblenWith_pos hf hp
139+
140+
theorem veblenWith_zero_lt_veblenWith_zero (hp : 0 < f 0) :
141+
veblenWith f o₁ 0 < veblenWith f o₂ 0 ↔ o₁ < o₂ :=
142+
(veblenWith_zero_strictMono hf hp).lt_iff_lt
143+
144+
theorem veblenWith_zero_le_veblenWith_zero (hp : 0 < f 0) :
145+
veblenWith f o₁ 0 ≤ veblenWith f o₂ 0 ↔ o₁ ≤ o₂ :=
146+
(veblenWith_zero_strictMono hf hp).le_iff_le
147+
148+
theorem veblenWith_zero_inj (hp : 0 < f 0) : veblenWith f o₁ 0 = veblenWith f o₂ 0 ↔ o₁ = o₂ :=
149+
(veblenWith_zero_strictMono hf hp).injective.eq_iff
150+
151+
theorem left_le_veblenWith (hp : 0 < f 0) (o a : Ordinal) : o ≤ veblenWith f o a :=
152+
(veblenWith_zero_strictMono hf hp).le_apply.trans <|
153+
(veblenWith_right_strictMono hf _).monotone (Ordinal.zero_le _)
154+
155+
theorem IsNormal.veblenWith_zero (hp : 0 < f 0) : IsNormal (veblenWith f · 0) := by
156+
rw [isNormal_iff_strictMono_limit]
157+
refine ⟨veblenWith_zero_strictMono hf hp, fun o ho a IH ↦ ?_⟩
158+
rw [veblenWith_of_ne_zero f ho.pos.ne', derivFamily_zero]
159+
apply nfpFamily_le fun l ↦ ?_
160+
suffices ∃ b < o, List.foldr _ 0 l ≤ veblenWith f b 0 by
161+
obtain ⟨b, hb, hb'⟩ := this
162+
exact hb'.trans (IH b hb)
163+
induction l with
164+
| nil => use 0; simp [ho.pos]
165+
| cons a l IH =>
166+
obtain ⟨b, hb, hb'⟩ := IH
167+
refine ⟨_, ho.succ_lt (max_lt a.2 hb), ((veblenWith_right_strictMono hf _).monotone <|
168+
hb'.trans <| veblenWith_left_monotone hf _ <|
169+
(le_max_right a.1 b).trans (Order.le_succ _)).trans ?_⟩
170+
rw [veblenWith_veblenWith_of_lt hf]
171+
rw [Order.lt_succ_iff]
172+
exact le_max_left _ b
173+
174+
theorem cmp_veblenWith :
175+
cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
176+
match cmp o₁ o₂ with
177+
| .eq => cmp a b
178+
| .lt => cmp a (veblenWith f o₂ b)
179+
| .gt => cmp (veblenWith f o₁ a) b := by
180+
obtain h | rfl | h := lt_trichotomy o₁ o₂
181+
on_goal 2 => simp [(veblenWith_right_strictMono hf _).cmp_map_eq]
182+
all_goals
183+
conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
184+
simp [h.cmp_eq_lt, h.cmp_eq_gt, h.ne, h.ne', (veblenWith_right_strictMono hf _).cmp_map_eq]
185+
186+
/-- `veblenWith f o₁ a < veblenWith f o₂ b` iff one of the following holds:
187+
* `o₁ = o₂` and `a < b`
188+
* `o₁ < o₂` and `a < veblenWith f o₂ b`
189+
* `o₁ > o₂` and `veblenWith f o₁ a < b` -/
190+
theorem veblenWith_lt_veblenWith_iff :
191+
veblenWith f o₁ a < veblenWith f o₂ b ↔
192+
o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b := by
193+
rw [← cmp_eq_lt_iff, cmp_veblenWith hf]
194+
aesop (add simp lt_asymm)
195+
196+
/-- `veblenWith f o₁ a ≤ veblenWith f o₂ b` iff one of the following holds:
197+
* `o₁ = o₂` and `a ≤ b`
198+
* `o₁ < o₂` and `a ≤ veblenWith f o₂ b`
199+
* `o₁ > o₂` and `veblenWith f o₁ a ≤ b` -/
200+
theorem veblenWith_le_veblenWith_iff :
201+
veblenWith f o₁ a ≤ veblenWith f o₂ b ↔
202+
o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b := by
203+
rw [← not_lt, ← cmp_eq_gt_iff, cmp_veblenWith hf]
204+
aesop (add simp [not_lt_of_le, lt_asymm])
205+
206+
/-- `veblenWith f o₁ a = veblenWith f o₂ b` iff one of the following holds:
207+
* `o₁ = o₂` and `a = b`
208+
* `o₁ < o₂` and `a = veblenWith f o₂ b`
209+
* `o₁ > o₂` and `veblenWith f o₁ a = b` -/
210+
theorem veblenWith_eq_veblenWith_iff :
211+
veblenWith f o₁ a = veblenWith f o₂ b ↔
212+
o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b := by
213+
rw [← cmp_eq_eq_iff, cmp_veblenWith hf]
214+
aesop (add simp lt_asymm)
215+
216+
end veblenWith
217+
218+
/-! ### Veblen function -/
219+
220+
section veblen
221+
222+
/-- `veblen o` is the `o`-th function in the Veblen hierarchy starting with `ω ^ ·`. That is:
223+
224+
- `veblen 0 a = ω ^ a`.
225+
- `veblen o` for `o ≠ 0` enumerates the fixed points of `veblen o'` for `o' < o`.
226+
-/
227+
@[pp_nodot]
228+
def veblen : Ordinal.{u} → Ordinal.{u} → Ordinal.{u} :=
229+
veblenWith (ω ^ ·)
230+
231+
@[simp]
232+
theorem veblen_zero : veblen 0 = fun a ↦ ω ^ a := by
233+
rw [veblen, veblenWith_zero]
234+
235+
theorem veblen_zero_apply (a : Ordinal) : veblen 0 a = ω ^ a := by
236+
rw [veblen_zero]
237+
238+
theorem veblen_of_ne_zero (h : o ≠ 0) : veblen o = derivFamily fun x : Set.Iio o ↦ veblen x.1 :=
239+
veblenWith_of_ne_zero _ h
240+
241+
theorem isNormal_veblen (o : Ordinal) : IsNormal (veblen o) :=
242+
(isNormal_opow one_lt_omega0).veblenWith o
243+
244+
theorem veblen_veblen_of_lt (h : o₁ < o₂) (a : Ordinal) : veblen o₁ (veblen o₂ a) = veblen o₂ a :=
245+
veblenWith_veblenWith_of_lt (isNormal_opow one_lt_omega0) h a
246+
247+
theorem veblen_succ (o : Ordinal) : veblen (Order.succ o) = deriv (veblen o) :=
248+
veblenWith_succ (isNormal_opow one_lt_omega0) o
249+
250+
theorem veblen_right_strictMono (o : Ordinal) : StrictMono (veblen o) :=
251+
veblenWith_right_strictMono (isNormal_opow one_lt_omega0) o
252+
253+
@[simp]
254+
theorem veblen_lt_veblen_iff_right : veblen o a < veblen o b ↔ a < b :=
255+
veblenWith_lt_veblenWith_iff_right (isNormal_opow one_lt_omega0)
256+
257+
@[simp]
258+
theorem veblen_le_veblen_iff_right : veblen o a ≤ veblen o b ↔ a ≤ b :=
259+
veblenWith_le_veblenWith_iff_right (isNormal_opow one_lt_omega0)
260+
261+
theorem veblen_injective (o : Ordinal) : Function.Injective (veblen o) :=
262+
veblenWith_injective (isNormal_opow one_lt_omega0) o
263+
264+
@[simp]
265+
theorem veblen_inj : veblen o a = veblen o b ↔ a = b :=
266+
(veblen_injective o).eq_iff
267+
268+
theorem right_le_veblen (o a : Ordinal) : a ≤ veblen o a :=
269+
right_le_veblenWith (isNormal_opow one_lt_omega0) o a
270+
271+
theorem veblen_left_monotone (o : Ordinal) : Monotone (veblen · o) :=
272+
veblenWith_left_monotone (isNormal_opow one_lt_omega0) o
273+
274+
@[simp]
275+
theorem veblen_pos : 0 < veblen o a :=
276+
veblenWith_pos (isNormal_opow one_lt_omega0) (by simp)
277+
278+
theorem veblen_zero_strictMono : StrictMono (veblen · 0) :=
279+
veblenWith_zero_strictMono (isNormal_opow one_lt_omega0) (by simp)
280+
281+
@[simp]
282+
theorem veblen_zero_lt_veblen_zero : veblen o₁ 0 < veblen o₂ 0 ↔ o₁ < o₂ :=
283+
veblen_zero_strictMono.lt_iff_lt
284+
285+
@[simp]
286+
theorem veblen_zero_le_veblen_zero : veblen o₁ 0 ≤ veblen o₂ 0 ↔ o₁ ≤ o₂ :=
287+
veblen_zero_strictMono.le_iff_le
288+
289+
@[simp]
290+
theorem veblen_zero_inj : veblen o₁ 0 = veblen o₂ 0 ↔ o₁ = o₂ :=
291+
veblen_zero_strictMono.injective.eq_iff
292+
293+
theorem left_le_veblen (o a : Ordinal) : o ≤ veblen o a :=
294+
left_le_veblenWith (isNormal_opow one_lt_omega0) (by simp) o a
295+
296+
theorem isNormal_veblen_zero : IsNormal (veblen · 0) :=
297+
(isNormal_opow one_lt_omega0).veblenWith_zero (by simp)
298+
299+
theorem cmp_veblen : cmp (veblen o₁ a) (veblen o₂ b) =
300+
match cmp o₁ o₂ with
301+
| .eq => cmp a b
302+
| .lt => cmp a (veblen o₂ b)
303+
| .gt => cmp (veblen o₁ a) b :=
304+
cmp_veblenWith (isNormal_opow one_lt_omega0)
305+
306+
/-- `veblen o₁ a < veblen o₂ b` iff one of the following holds:
307+
* `o₁ = o₂` and `a < b`
308+
* `o₁ < o₂` and `a < veblen o₂ b`
309+
* `o₁ > o₂` and `veblen o₁ a < b` -/
310+
theorem veblen_lt_veblen_iff :
311+
veblen o₁ a < veblen o₂ b ↔
312+
o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a < b :=
313+
veblenWith_lt_veblenWith_iff (isNormal_opow one_lt_omega0)
314+
315+
/-- `veblen o₁ a ≤ veblen o₂ b` iff one of the following holds:
316+
* `o₁ = o₂` and `a ≤ b`
317+
* `o₁ < o₂` and `a ≤ veblen o₂ b`
318+
* `o₁ > o₂` and `veblen o₁ a ≤ b` -/
319+
theorem veblen_le_veblen_iff :
320+
veblen o₁ a ≤ veblen o₂ b ↔
321+
o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a ≤ b :=
322+
veblenWith_le_veblenWith_iff (isNormal_opow one_lt_omega0)
323+
324+
/-- `veblen o₁ a ≤ veblen o₂ b` iff one of the following holds:
325+
* `o₁ = o₂` and `a = b`
326+
* `o₁ < o₂` and `a = veblen o₂ b`
327+
* `o₁ > o₂` and `veblen o₁ a = b` -/
328+
theorem veblen_eq_veblen_iff :
329+
veblen o₁ a = veblen o₂ b ↔
330+
o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a = b :=
331+
veblenWith_eq_veblenWith_iff (isNormal_opow one_lt_omega0)
332+
333+
end veblen
334+
end Ordinal

0 commit comments

Comments
 (0)