Skip to content

Commit

Permalink
move(set_theory/ordinal/{arithmetic → fixed_points}): Move nfp (#13315
Browse files Browse the repository at this point in the history 
)

That way, it belong with the other functions about fixed points.
  • Loading branch information
@vihdzp
vihdzp committed May 4, 2022
1 parent 1a86249 commit e24f7f7
Show file tree
Hide file tree
Showing 3 changed files with 298 additions and 310 deletions.
298 changes: 0 additions & 298 deletions src/set_theory/ordinal/arithmetic.lean
View file
Expand Up @@ -40,8 +40,6 @@ Some properties of the operations are also used to discuss general tools on ordi
and order-continuous, i.e., the image `f o` of a limit ordinal `o` is the sup of `f a` for
`a < o`.
* `enum_ord`: enumerates an unbounded set of ordinals by the ordinals themselves.
* `nfp f a`: the next fixed point of a function `f` on ordinals, above `a`. It behaves well
for normal functions.
* `CNF b o` is the Cantor normal form of the ordinal `o` in base `b`.
* `sup`, `lsub`: the supremum / least strict upper bound of an indexed family of ordinals in
`Type u`, as an ordinal in `Type u`.
Expand Down Expand Up @@ -2420,300 +2418,4 @@ begin
rw [nat.cast_zero, opow_zero] }
end

/-! ### Fixed points of normal functions -/

section
variable {f : ordinal.{u} → ordinal.{u}}

/-- The next fixed point function, the least fixed point of the normal function `f` above `a`. -/
def nfp (f : ordinal → ordinal) (a : ordinal) :=
sup (λ n : ℕ, f^[n] a)

theorem nfp_le_iff {f a b} : nfp f a ≤ b ↔ ∀ n, f^[n] a ≤ b :=
sup_le_iff

theorem nfp_le {f a b} : (∀ n, f^[n] a ≤ b) → nfp f a ≤ b :=
sup_le

theorem iterate_le_nfp (f a n) : f^[n] a ≤ nfp f a :=
le_sup _ n

theorem le_nfp_self (f a) : a ≤ nfp f a :=
iterate_le_nfp f a 0

theorem lt_nfp {f : ordinal → ordinal} {a b} : a < nfp f b ↔ ∃ n, a < (f^[n]) b :=
lt_sup

protected theorem is_normal.lt_nfp {f} (H : is_normal f) {a b} : f b < nfp f a ↔ b < nfp f a :=
lt_nfp.trans $ iff.trans
(by exact
⟨λ ⟨n, h⟩, ⟨n, lt_of_le_of_lt (H.self_le _) h⟩,
λ ⟨n, h⟩, ⟨n+1, by rw iterate_succ'; exact H.lt_iff.2 h⟩⟩)
lt_sup.symm

protected theorem is_normal.nfp_le (H : is_normal f) {a b} : nfp f a ≤ f b ↔ nfp f a ≤ b :=
le_iff_le_iff_lt_iff_lt.2 H.lt_nfp

theorem is_normal.nfp_le_fp (H : is_normal f) {a b} (ab : a ≤ b) (h : f b ≤ b) : nfp f a ≤ b :=
nfp_le $ λ i, begin
induction i with i IH generalizing a, {exact ab},
exact IH (le_trans (H.le_iff.2 ab) h),
end

theorem is_normal.nfp_fp (H : is_normal f) (a) : f (nfp f a) = nfp f a :=
begin
refine le_antisymm _ (H.self_le _),
cases le_or_lt (f a) a with aa aa,
{ rwa le_antisymm (H.nfp_le_fp le_rfl aa) (le_nfp_self _ _) },
rcases zero_or_succ_or_limit (nfp f a) with e|⟨b, e⟩|l,
{ refine @le_trans _ _ _ (f a) _ (H.le_iff.2 _) (iterate_le_nfp f a 1),
simp only [e, ordinal.zero_le] },
{ have : f b < nfp f a := H.lt_nfp.2 (by simp only [e, lt_succ_self]),
rw [e, lt_succ] at this,
have ab : a ≤ b,
{ rw [← lt_succ, ← e],
exact lt_of_lt_of_le aa (iterate_le_nfp f a 1) },
refine le_trans (H.le_iff.2 (H.nfp_le_fp ab this))
(le_trans this (le_of_lt _)),
simp only [e, lt_succ_self] },
{ exact (H.2 _ l _).2 (λ b h, le_of_lt (H.lt_nfp.2 h)) }
end

theorem is_normal.le_nfp (H : is_normal f) {a b} : f b ≤ nfp f a ↔ b ≤ nfp f a :=
⟨le_trans (H.self_le _), λ h, by simpa only [H.nfp_fp] using H.le_iff.2 h⟩

theorem nfp_eq_self {a} (h : f a = a) : nfp f a = a :=
(nfp_le $ λ i, by rw [iterate_fixed h]).antisymm (le_nfp_self f a)

protected lemma monotone.nfp (hf : monotone f) : monotone (nfp f) :=
λ a b h, nfp_le (λ n, (hf.iterate n h).trans (le_sup _ n))

/-- Fixed point lemma for normal functions: the fixed points of a normal function are unbounded. -/
theorem is_normal.nfp_unbounded {f} (H : is_normal f) : unbounded (<) (fixed_points f) :=
λ a, ⟨_, H.nfp_fp a, not_lt_of_ge (le_nfp_self f a)⟩

/-- The derivative of a normal function `f` is the sequence of fixed points of `f`. -/
def deriv (f : ordinal → ordinal) (o : ordinal) : ordinal :=
limit_rec_on o (nfp f 0)
(λ a IH, nfp f (succ IH))
(λ a l, bsup.{u u} a)

@[simp] theorem deriv_zero (f) : deriv f 0 = nfp f 0 := limit_rec_on_zero _ _ _

@[simp] theorem deriv_succ (f o) : deriv f (succ o) = nfp f (succ (deriv f o)) :=
limit_rec_on_succ _ _ _ _

theorem deriv_limit (f) {o} : is_limit o → deriv f o = bsup.{u u} o (λ a _, deriv f a) :=
limit_rec_on_limit _ _ _ _

theorem deriv_is_normal (f) : is_normal (deriv f) :=
⟨λ o, by rw [deriv_succ, ← succ_le]; apply le_nfp_self,
λ o l a, by rw [deriv_limit _ l, bsup_le_iff]⟩

theorem is_normal.deriv_fp (H : is_normal f) (o) : f (deriv.{u} f o) = deriv f o :=
begin
apply limit_rec_on o,
{ rw [deriv_zero, H.nfp_fp] },
{ intros o ih, rw [deriv_succ, H.nfp_fp] },
intros o l IH,
rw [deriv_limit _ l, is_normal.bsup.{u u u} H _ l.1],
refine eq_of_forall_ge_iff (λ c, _),
simp only [bsup_le_iff, IH] {contextual:=tt}
end

theorem is_normal.le_iff_deriv (H : is_normal f) {a} : f a ≤ a ↔ ∃ o, deriv f o = a :=
⟨λ ha, begin
suffices : ∀ o (_ : a ≤ deriv f o), ∃ o, deriv f o = a,
from this a ((deriv_is_normal _).self_le _),
refine λ o, limit_rec_on o (λ h₁, ⟨0, le_antisymm _ h₁⟩) (λ o IH h₁, _) (λ o l IH h₁, _),
{ rw deriv_zero,
exact H.nfp_le_fp (ordinal.zero_le _) ha },
{ cases le_or_lt a (deriv f o), {exact IH h},
refine ⟨succ o, le_antisymm _ h₁⟩,
rw deriv_succ,
exact H.nfp_le_fp (succ_le.2 h) ha },
{ cases eq_or_lt_of_le h₁, {exact ⟨_, h.symm⟩},
rw [deriv_limit _ l, ← not_le, bsup_le_iff, not_ball] at h,
exact let ⟨o', h, hl⟩ := h in IH o' h (le_of_not_le hl) }
end, λ ⟨o, e⟩, e ▸ le_of_eq (H.deriv_fp _)⟩

theorem is_normal.apply_eq_self_iff_deriv (H : is_normal f) {a} : f a = a ↔ ∃ o, deriv f o = a :=
by rw [←H.le_iff_deriv, H.le_iff_eq]

/-- `deriv f` is the fixed point enumerator of `f`. -/
theorem deriv_eq_enum_fp {f} (H : is_normal f) : deriv f = enum_ord (fixed_points f) :=
begin
rw [←eq_enum_ord _ H.nfp_unbounded, range_eq_iff],
exact ⟨(deriv_is_normal f).strict_mono, H.deriv_fp, λ _, H.apply_eq_self_iff_deriv.1⟩
end

theorem deriv_eq_id_of_nfp_eq_id {f : ordinal → ordinal} (h : nfp f = id) : deriv f = id :=
(is_normal.eq_iff_zero_and_succ (deriv_is_normal _) is_normal.refl).2 (by simp [h, succ_inj])

end

/-! ### Fixed points of addition -/

@[simp] theorem nfp_add_zero (a) : nfp ((+) a) 0 = a * omega :=
begin
unfold nfp,
rw ←sup_mul_nat,
congr, funext,
induction n with n hn,
{ rw [nat.cast_zero, mul_zero, iterate_zero_apply] },
{ nth_rewrite 1 nat.succ_eq_one_add,
rw [nat.cast_add, nat.cast_one, mul_one_add, iterate_succ_apply', hn] }
end

theorem nfp_add_eq_mul_omega {a b} (hba : b ≤ a * omega) :
nfp ((+) a) b = a * omega :=
begin
apply le_antisymm ((add_is_normal a).nfp_le_fp hba _),
{ rw ←nfp_add_zero,
exact monotone.nfp (add_is_normal a).monotone (ordinal.zero_le b) },
{ rw [←mul_one_add, one_add_omega] }
end

theorem add_eq_right_iff_mul_omega_le {a b : ordinal} : a + b = b ↔ a * omega ≤ b :=
begin
refine ⟨λ h, _, λ h, _⟩,
{ rw [←nfp_add_zero a, ←deriv_zero],
cases (add_is_normal a).apply_eq_self_iff_deriv.1 h with c hc,
rw ←hc,
exact (deriv_is_normal _).monotone (ordinal.zero_le _) },
{ have := ordinal.add_sub_cancel_of_le h,
nth_rewrite 0 ←this,
rwa [←add_assoc, ←mul_one_add, one_add_omega] }
end

theorem add_le_right_iff_mul_omega_le {a b : ordinal} : a + b ≤ b ↔ a * omega ≤ b :=
by { rw ←add_eq_right_iff_mul_omega_le, exact (add_is_normal a).le_iff_eq }

theorem deriv_add_eq_mul_omega_add (a b : ordinal.{u}) : deriv ((+) a) b = a * omega + b :=
begin
revert b,
rw [←funext_iff, is_normal.eq_iff_zero_and_succ (deriv_is_normal _) (add_is_normal _)],
refine ⟨_, λ a h, _⟩,
{ rw [deriv_zero, add_zero],
exact nfp_add_zero a },
{ rw [deriv_succ, h, add_succ],
exact nfp_eq_self (add_eq_right_iff_mul_omega_le.2 ((le_add_right _ _).trans
(lt_succ_self _).le)) }
end

/-! ### Fixed points of multiplication -/

@[simp] theorem nfp_mul_one {a : ordinal} (ha : 0 < a) : nfp ((*) a) 1 = a ^ omega :=
begin
unfold nfp,
rw ←sup_opow_nat,
{ congr,
funext,
induction n with n hn,
{ rw [nat.cast_zero, opow_zero, iterate_zero_apply] },
nth_rewrite 1 nat.succ_eq_one_add,
rw [nat.cast_add, nat.cast_one, opow_add, opow_one, iterate_succ_apply', hn] },
{ exact ha }
end

@[simp] theorem nfp_mul_zero (a : ordinal) : nfp ((*) a) 0 = 0 :=
begin
rw [←ordinal.le_zero, nfp_le_iff],
intro n,
induction n with n hn, { refl },
rwa [iterate_succ_apply, mul_zero]
end

@[simp] theorem nfp_zero_mul : nfp ((*) 0) = id :=
begin
refine funext (λ a, (nfp_le (λ n, _)).antisymm (le_sup (λ n, ((*) 0)^[n] a) 0)),
induction n with n hn, { refl },
rw function.iterate_succ',
change 0 * _ ≤ a,
rw zero_mul,
exact ordinal.zero_le a
end

@[simp] theorem deriv_mul_zero : deriv ((*) 0) = id :=
deriv_eq_id_of_nfp_eq_id nfp_zero_mul

theorem nfp_mul_eq_opow_omega {a b : ordinal} (hb : 0 < b) (hba : b ≤ a ^ omega) :
nfp ((*) a) b = a ^ omega.{u} :=
begin
cases eq_zero_or_pos a with ha ha,
{ rw [ha, zero_opow omega_ne_zero] at *,
rw [ordinal.le_zero.1 hba, nfp_zero_mul],
refl },
apply le_antisymm,
{ apply (mul_is_normal ha).nfp_le_fp hba,
rw [←opow_one_add, one_add_omega] },
rw ←nfp_mul_one ha,
exact monotone.nfp (mul_is_normal ha).monotone (one_le_iff_pos.2 hb)
end

theorem eq_zero_or_opow_omega_le_of_mul_eq_right {a b : ordinal} (hab : a * b = b) :
b = 0 ∨ a ^ omega.{u} ≤ b :=
begin
cases eq_zero_or_pos a with ha ha,
{ rw [ha, zero_opow omega_ne_zero],
exact or.inr (ordinal.zero_le b) },
rw or_iff_not_imp_left,
intro hb,
change b ≠ 0 at hb,
rw ←nfp_mul_one ha,
rw ←one_le_iff_ne_zero at hb,
exact (mul_is_normal ha).nfp_le_fp hb (le_of_eq hab)
end

theorem mul_eq_right_iff_opow_omega_dvd {a b : ordinal} : a * b = b ↔ a ^ omega ∣ b :=
begin
cases eq_zero_or_pos a with ha ha,
{ rw [ha, zero_mul, zero_opow omega_ne_zero, zero_dvd],
exact eq_comm },
refine ⟨λ hab, _, λ h, _⟩,
{ rw dvd_iff_mod_eq_zero,
rw [←div_add_mod b (a ^ omega), mul_add, ←mul_assoc, ←opow_one_add, one_add_omega,
add_left_cancel] at hab,
cases eq_zero_or_opow_omega_le_of_mul_eq_right hab with hab hab,
{ exact hab },
refine (not_lt_of_le hab (mod_lt b (opow_ne_zero omega _))).elim,
rwa ←ordinal.pos_iff_ne_zero },
cases h with c hc,
rw [hc, ←mul_assoc, ←opow_one_add, one_add_omega]
end

theorem mul_le_right_iff_opow_omega_dvd {a b : ordinal} (ha : 0 < a) : a * b ≤ b ↔ a ^ omega ∣ b :=
by { rw ←mul_eq_right_iff_opow_omega_dvd, exact (mul_is_normal ha).le_iff_eq }

theorem nfp_mul_opow_omega_add {a c : ordinal} (b) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ a ^ omega) :
nfp ((*) a) (a ^ omega * b + c) = a ^ omega.{u} * b.succ :=
begin
apply le_antisymm,
{ apply is_normal.nfp_le_fp (mul_is_normal ha),
{ rw mul_succ,
apply add_le_add_left hca },
{ rw [←mul_assoc, ←opow_one_add, one_add_omega] } },
{ cases mul_eq_right_iff_opow_omega_dvd.1 ((mul_is_normal ha).nfp_fp (a ^ omega * b + c))
with d hd,
rw hd,
apply mul_le_mul_left',
have := le_nfp_self (has_mul.mul a) (a ^ omega * b + c),
rw hd at this,
have := (add_lt_add_left hc (a ^ omega * b)).trans_le this,
rw [add_zero, mul_lt_mul_iff_left (opow_pos omega ha)] at this,
rwa succ_le }
end

theorem deriv_mul_eq_opow_omega_mul {a : ordinal.{u}} (ha : 0 < a) (b) :
deriv ((*) a) b = a ^ omega * b :=
begin
revert b,
rw [←funext_iff,
is_normal.eq_iff_zero_and_succ (deriv_is_normal _) (mul_is_normal (opow_pos omega ha))],
refine ⟨_, λ c h, _⟩,
{ rw [deriv_zero, nfp_mul_zero, mul_zero] },
{ rw [deriv_succ, h],
exact nfp_mul_opow_omega_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha)) },
end

end ordinal

0 comments on commit e24f7f7

Please sign in to comment.