IsNormal.lean

/-
Copyright (c) 2025 Violeta Hernández Palacios. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Violeta Hernández Palacios
-/
module

public import Mathlib.Dynamics.FixedPoints.Defs
public import Mathlib.Order.DirSupClosed.Basic
public import Mathlib.Order.SuccPred.CompleteLinearOrder
public import Mathlib.Order.SuccPred.InitialSeg

/-!
# Normal functions

A normal function between well-orders is a strictly monotonic continuous function. Normal functions
arise chiefly in the context of cardinal and ordinal-valued functions.

We opt for an equivalent definition that's both simpler and often more convenient: a normal function
is a strictly monotonic function `f` such that at successor limits `a`, `f a` is the least upper
bound of `f b` with `b < a`.

See `Order.isNormal_iff_strictMono_and_continuous` for a proof that these notions are equivalent.
-/

public section

open Set

variable {α β γ : Type*} {a b : α} {f : α → β} {g : β → γ}

namespace Order

/-- A normal function between well-orders is a strictly monotonic continuous function. -/
@[mk_iff isNormal_iff']
structure IsNormal [LinearOrder α] [LinearOrder β] (f : α → β) : Prop where
  strictMono : StrictMono f
  /-- This condition is the RHS of the `IsLUB (f '' Iio a) (f a)` predicate, which is sufficient
  since the LHS is implied by monotonicity. -/
  mem_lowerBounds_upperBounds_of_isSuccLimit {a : α} (ha : IsSuccLimit a) :
    f a ∈ lowerBounds (upperBounds (f '' Iio a))

theorem isNormal_iff [LinearOrder α] [LinearOrder β] {f : α → β} :
    IsNormal f ↔ StrictMono f ∧ ∀ o, IsSuccLimit o → ∀ a, (∀ b < o, f b ≤ a) → f o ≤ a := by
  simp [isNormal_iff', mem_lowerBounds, mem_upperBounds]

namespace IsNormal

section LinearOrder
variable [LinearOrder α] [LinearOrder β] [LinearOrder γ]

protected theorem monotone {f : α → β} (hf : IsNormal f) : Monotone f :=
  hf.strictMono.monotone

theorem isLUB_image_Iio_of_isSuccLimit {f : α → β} (hf : IsNormal f) {a : α} (ha : IsSuccLimit a) :
    IsLUB (f '' Iio a) (f a) := by
  refine ⟨?_, hf.2 ha⟩
  rintro - ⟨b, hb, rfl⟩
  exact (hf.1 hb).le

theorem le_iff_forall_le (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
    f a ≤ b ↔ ∀ a' < a, f a' ≤ b := by
  simpa [mem_upperBounds] using isLUB_le_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)

theorem lt_iff_exists_lt (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
    b < f a ↔ ∃ a' < a, b < f a' := by
  simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)

theorem map_isSuccLimit (hf : IsNormal f) (ha : IsSuccLimit a) : IsSuccLimit (f a) := by
  refine ⟨?_, fun b hb ↦ ?_⟩
  · obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin
    exact not_isMin_iff.2 ⟨_, hf.strictMono hb⟩
  · obtain ⟨c, hc, hc'⟩ := (hf.lt_iff_exists_lt ha).1 hb.lt
    have hc' := hb.ge_of_gt hc'
    rw [hf.strictMono.le_iff_le] at hc'
    exact hc.not_ge hc'

theorem map_isLUB (hf : IsNormal f) {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) :
    IsLUB (f '' s) (f a) := by
  refine ⟨?_, fun b hb ↦ ?_⟩
  · simpa [mem_upperBounds, hf.strictMono.le_iff_le] using hs.1
  · by_cases ha : a ∈ s
    · simp_all [mem_upperBounds]
    · have ha' := hs.isSuccLimit_of_notMem hs' ha
      rw [le_iff_forall_le hf ha']
      intro c hc
      obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc
      simp_rw [mem_upperBounds, forall_mem_image] at hb
      exact (hf.strictMono hcd).le.trans (hb hd)

theorem _root_.InitialSeg.isNormal (f : α ≤i β) : IsNormal f where
  strictMono := f.strictMono
  mem_lowerBounds_upperBounds_of_isSuccLimit ha := by
    rw [f.image_Iio]
    exact (f.map_isSuccLimit ha).isLUB_Iio.2

theorem _root_.PrincipalSeg.isNormal (f : α <i β) : IsNormal f :=
  (f : α ≤i β).isNormal

theorem _root_.OrderIso.isNormal (f : α ≃o β) : IsNormal f :=
  f.toInitialSeg.isNormal

protected theorem id : IsNormal (@id α) :=
  (OrderIso.refl _).isNormal

theorem comp (hg : IsNormal g) (hf : IsNormal f) : IsNormal (g ∘ f) := by
  refine ⟨hg.strictMono.comp hf.strictMono, fun ha b hb ↦ ?_⟩
  simp_rw [Function.comp_apply, mem_upperBounds, forall_mem_image] at hb
  simpa [hg.le_iff_forall_le (hf.map_isSuccLimit ha), hf.lt_iff_exists_lt ha] using
    fun c d hd hc ↦ (hg.strictMono hc).le.trans (hb hd)

/-- Restrict a normal function `α → β` to a normal function `Iio a → Iio (f a)`. -/
theorem to_Iio (hf : IsNormal f) (a : α) :
    IsNormal (β := Iio (f a)) fun x : Iio a ↦ ⟨f x.1, hf.strictMono x.2⟩ := by
  rw [isNormal_iff]
  refine ⟨fun x y h ↦ hf.strictMono h, fun b hb c hc ↦ hf.2 (hb.subtypeVal (isLowerSet_Iio _)) ?_⟩
  simpa [upperBounds] using! fun d hd ↦ hc ⟨d, hd.trans b.2⟩ hd

end LinearOrder

section ConditionallyCompleteLinearOrder
variable [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β]

theorem map_sSup (hf : IsNormal f) {s : Set α} (hs : s.Nonempty) (hs' : BddAbove s) :
    f (sSup s) = sSup (f '' s) :=
  ((hf.map_isLUB (isLUB_csSup hs hs') hs).csSup_eq (hs.image f)).symm

theorem map_iSup {ι} [Nonempty ι] {g : ι → α} (hf : IsNormal f) (hg : BddAbove (range g)) :
    f (⨆ i, g i) = ⨆ i, f (g i) := by
  unfold iSup
  convert! map_sSup hf (range_nonempty g) hg
  ext
  simp

theorem iSup_iterate_mem_fixedPoints [WellFoundedLT α] {f : α → α} (a : α) (hf : IsNormal f)
    (hf' : BddAbove (.range fun n ↦ f^[n] a)) : ⨆ n, f^[n] a ∈ f.fixedPoints := by
  rw [f.mem_fixedPoints_iff, hf.map_iSup hf']
  apply le_antisymm <;> refine ciSup_le fun n ↦ ?_
  · rw [← f.iterate_succ_apply']
    exact le_ciSup hf' _
  · apply hf.strictMono.le_apply.trans
    apply (le_ciSup (hf'.mono _) n)
    simp_rw [← f.iterate_succ_apply']
    grind

theorem preimage_Iic (hf : IsNormal f) {x : β}
    (h₁ : (f ⁻¹' Iic x).Nonempty) (h₂ : BddAbove (f ⁻¹' Iic x)) :
    f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x)) := by
  refine le_antisymm (fun _ ↦ le_csSup h₂) (fun y hy ↦ ?_)
  obtain hy | rfl := hy.lt_or_eq
  · rw [lt_csSup_iff h₂ h₁] at hy
    obtain ⟨z, hz, hyz⟩ := hy
    exact (hf.strictMono hyz).le.trans hz
  · rw [mem_preimage, hf.map_sSup h₁ h₂]
    apply (csSup_le_csSup bddAbove_Iic _ (image_preimage_subset ..)).trans
    · rw [csSup_Iic]
    · simpa

theorem le_iff_le_sSup (hf : IsNormal f) {x : α} {y : β}
    (h₁ : (f ⁻¹' Iic y).Nonempty) (h₂ : BddAbove (f ⁻¹' Iic y)) :
    f x ≤ y ↔ x ≤ sSup (f ⁻¹' Iic y) :=
  Set.ext_iff.1 (preimage_Iic hf h₁ h₂) x

/-- If `f : α → α` in a well-order, we can infer one of the hypotheses in
`Order.IsNormal.le_iff_le_sSup`. -/
theorem le_iff_le_sSup' [WellFoundedLT α] {f : α → α} (hf : IsNormal f) {x y : α}
    (h : (f ⁻¹' Iic y).Nonempty) : f x ≤ y ↔ x ≤ sSup (f ⁻¹' Iic y) :=
  hf.le_iff_le_sSup h ⟨y, fun _ ↦ hf.strictMono.le_apply.trans⟩

end ConditionallyCompleteLinearOrder

section ConditionallyCompleteLinearOrderBot
variable [ConditionallyCompleteLinearOrderBot α] [ConditionallyCompleteLinearOrder β]

theorem apply_of_isSuccLimit (hf : IsNormal f) (ha : IsSuccLimit a) :
    f a = ⨆ b : Iio a, f b := by
  convert! map_iSup hf _
  · exact ha.iSup_Iio.symm
  · exact ⟨⊥, ha.bot_lt⟩
  · use a
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    exact hx.le

end ConditionallyCompleteLinearOrderBot

section WellFoundedLT
variable [LinearOrder α] [WellFoundedLT α] [SuccOrder α] [LinearOrder β]

theorem of_succ_lt
    (hs : ∀ a, f a < f (succ a)) (hl : ∀ {a}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)) :
    IsNormal f := by
  refine ⟨fun a b ↦ ?_, fun ha ↦ (hl ha).2⟩
  induction b using SuccOrder.limitRecOn with
  | isMin b hb => exact hb.not_lt.elim
  | succ b hb IH =>
    intro hab
    obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
    · exact hs a
    · exact (IH h).trans (hs b)
  | isSuccLimit b hb IH =>
    intro hab
    have hab' := hb.succ_lt hab
    exact (IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le
      ((hl hb).1 (mem_image_of_mem _ hab'))

theorem ext_iff [OrderBot α] {g : α → β} (hf : IsNormal f) (hg : IsNormal g) :
    f = g ↔ f ⊥ = g ⊥ ∧ ∀ a, f a = g a → f (succ a) = g (succ a) := by
  constructor
  · simp_all
  rintro ⟨H₁, H₂⟩
  ext a
  induction a using SuccOrder.limitRecOn with
  | isMin a ha => rw [ha.eq_bot, H₁]
  | succ a ha IH => exact H₂ a IH
  | isSuccLimit a ha IH =>
    apply (hf.isLUB_image_Iio_of_isSuccLimit ha).unique
    convert! hg.isLUB_image_Iio_of_isSuccLimit ha using 1
    aesop

@[deprecated (since := "2026-03-22")] protected alias ext := IsNormal.ext_iff

theorem exists_map_le_lt_map_succ_of_exists_ge [NoMaxOrder α] [OrderBot α] [WellFoundedLT β]
    {f : α → β} {x : β} (hf : IsNormal f) (hf' : ∃ y, x ≤ f y) (hx : f ⊥ ≤ x) :
    ∃ a, f a ≤ x ∧ x < f (succ a) := by
  have : Nonempty β := ⟨x⟩
  let := WellFoundedLT.toOrderBot β
  let := WellFoundedLT.conditionallyCompleteLinearOrderBot α
  let := WellFoundedLT.conditionallyCompleteLinearOrderBot β
  have H : BddAbove (f ⁻¹' Iic x) :=
    have ⟨y, hy⟩ := hf'
    ⟨y, fun z hz ↦ hf.strictMono.le_iff_le.1 <| hz.trans hy⟩
  refine ⟨sSup (f ⁻¹' Set.Iic x), ?_, ?_⟩
  · rw [hf.le_iff_le_sSup ⟨⊥, hx⟩ H]
  · rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]

/-- If `f : α → α`, we can infer one of the hypotheses in
`exists_map_le_lt_map_succ_of_exists_ge`. -/
theorem exists_map_le_lt_map_succ [NoMaxOrder α] [OrderBot α] {f : α → α} {x : α}
    (hf : IsNormal f) (hx : f ⊥ ≤ x) : ∃ a, f a ≤ x ∧ x < f (succ a) :=
  exists_map_le_lt_map_succ_of_exists_ge hf ⟨x, hf.strictMono.le_apply⟩ hx

omit [SuccOrder α] in
theorem dirSupClosed_range {f : α → α} (hf : IsNormal f) : DirSupClosed (range f) := by
  intro s hs hs₀ _ a ha
  have hf' : (f ⁻¹' s).Nonempty := by
    obtain ⟨b, hb⟩ := hs₀
    obtain ⟨c, rfl⟩ := hs hb
    exact ⟨c, hb⟩
  have : Nonempty α := ⟨a⟩
  let := WellFoundedLT.toOrderBot α
  let := WellFoundedLT.conditionallyCompleteLinearOrderBot α
  have hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s)) :=
    isLUB_csSup hf' ⟨a, fun b hb ↦ hf.strictMono.le_apply.trans (ha.1 hb)⟩
  have ha' := hf.map_isLUB hfl hf'
  rw [image_preimage_eq_of_subset hs] at ha'
  obtain rfl := ha.unique ha'
  exact mem_range_self _

end WellFoundedLT
end IsNormal
end Order