SignTermination.lean

1import BFPP.SignRecursion2import Mathlib.Order.WellFounded34/-! # Termination at a limit ordinal -/56namespace BFPP78set_option autoImplicit false910open Set Order1112universe u13variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [NormalSpace K]1415theorem signRecursion_ne_of_lt (seed : UnitBall C(K, ℝ)) (p q : K)16    (hpq : ClopenInseparable p q) (hp : seed.val p = 1) (hq : seed.val q = -1)17    (a b : Ordinal.{u}) (ha₁ : 1 ≤ a) (hab : a < b)18    (ha : SignStageGood seed a) (hb : SignStageGood seed b) :19    signRecursion seed a ≠ signRecursion seed b := by20  have hpoints := signRecursion_at_points seed p q hp hq a ha₁ ha21  obtain ⟨t, ht₀, ht₁⟩ := exists_intermediate_value_of_clopenInseparable p q hpq22    (signRecursion seed a) hpoints.1 hpoints.223  intro heq24  have heval := congrArg (fun h : UnitBall C(K, ℝ) => h.val t) heq25  rcases lt_or_gt_of_ne (abs_pos.mp ht₀) with hneg | hpos26  · have ht := signRecursion_negative_saturated seed a b hab hb t hneg27    rw [heval, ht] at ht₁28    norm_num at ht₁29  · have ht := signRecursion_positive_saturated seed a b hab hb t hpos30    rw [heval, ht] at ht₁31    norm_num at ht₁3233theorem exists_bad_signStage (seed : UnitBall C(K, ℝ)) (p q : K)34    (hpq : ClopenInseparable p q) (hp : seed.val p = 1) (hq : seed.val q = -1) :35    ∃ a : Ordinal.{u}, ¬ SignStageGood seed a := by36  by_contra hnone37  have hgood : ∀ a : Ordinal.{u}, SignStageGood seed a := by38    intro a39    by_contra ha40    exact hnone ⟨a, ha⟩41  let f : Ordinal.{u} → UnitBall C(K, ℝ) := fun a => signRecursion seed (Order.succ a)42  have hsucc (a : Ordinal.{u}) : (1 : Ordinal.{u}) ≤ Order.succ a := by43    simpa using (Order.succ_le_succ (show (0 : Ordinal.{u}) ≤ a from bot_le))44  have hinj : Function.Injective f := by45    intro a b hab46    rcases lt_trichotomy a b with hlt | heq | hgt47    · exact (signRecursion_ne_of_lt seed p q hpq hp hq _ _ (hsucc a)48        (Order.succ_lt_succ hlt) (hgood _) (hgood _) hab).elim49    · exact heq50    · exact (signRecursion_ne_of_lt seed p q hpq hp hq _ _ (hsucc b)51        (Order.succ_lt_succ hgt) (hgood _) (hgood _) hab.symm).elim52  exact no_injection_from_ordinals _ f hinj5354theorem exists_first_bad_limit (hK : IsFSpace K) (seed : UnitBall C(K, ℝ)) (p q : K)55    (hpq : ClopenInseparable p q) (hp : seed.val p = 1) (hq : seed.val q = -1) :56    ∃ d : Ordinal.{u}, IsSuccLimit d ∧ ¬ SignStageGood seed d ∧57      ∀ a, a < d → SignStageGood seed a := by58  obtain ⟨d, hd, hmin⟩ := Ordinal.lt_wf.has_min {a | ¬ SignStageGood seed a}59    (exists_bad_signStage seed p q hpq hp hq)60  have hbefore : ∀ a, a < d → SignStageGood seed a := by61    intro a had62    by_contra ha63    exact hmin a ha had64  have hd₀ : d ≠ 0 := by65    intro h66    subst d67    exact hd (signStageGood_zero seed)68  refine ⟨d, ?_, hd, hbefore⟩69  refine ⟨?_, ?_⟩70  · intro h71    exact hd₀ h.eq_bot72  · intro a hacov73    have heq : Order.succ a = d := Order.succ_eq_iff_covBy.mpr hacov74    have hs := signStageGood_succ hK seed a (hbefore a hacov.lt)75    rw [heq] at hs76    exact hd hs7778end BFPP

SHA-256