SignRecursion.lean

1import BFPP.SignExtension2import BFPP.Hartogs3import Mathlib.SetTheory.Ordinal.Arithmetic45/-! # The transfinite sign-extension recursion -/67namespace BFPP89set_option autoImplicit false1011open Set Order1213universe u14variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [NormalSpace K]1516def zeroBall : UnitBall C(K, ℝ) := ⟨0, by simp⟩1718def signsPositiveBefore (H : Ordinal.{u} → UnitBall C(K, ℝ)) (a : Ordinal.{u}) : Set K :=19  ⋃ b : Iio a, {t | 0 < (H b.val).val t}2021def signsNegativeBefore (H : Ordinal.{u} → UnitBall C(K, ℝ)) (a : Ordinal.{u}) : Set K :=22  ⋃ b : Iio a, {t | (H b.val).val t < 0}2324noncomputable def signRecursionStep (seed : UnitBall C(K, ℝ)) (a : Ordinal.{u})25    (previous : ∀ b, b < a → UnitBall C(K, ℝ)) : UnitBall C(K, ℝ) := by26  classical27  let U : Set K := ⋃ b : Iio a, {t | 0 < (previous b.val b.property).val t}28  let V : Set K := ⋃ b : Iio a, {t | (previous b.val b.property).val t < 0}29  exact if a = 0 then zeroBall else if a = 1 then seed else30    if h : Disjoint (closure U) (closure V) then (exists_sign_extension U V h).choose else zeroBall3132noncomputable def signRecursion (seed : UnitBall C(K, ℝ)) : Ordinal.{u} → UnitBall C(K, ℝ) :=33  Ordinal.lt_wf.fix (signRecursionStep seed)3435theorem signRecursion_eq (seed : UnitBall C(K, ℝ)) (a : Ordinal.{u}) :36    signRecursion seed a = signRecursionStep seed a (fun b _ => signRecursion seed b) :=37  WellFounded.fix_eq _ _ _3839@[simp] theorem signRecursion_zero (seed : UnitBall C(K, ℝ)) : signRecursion seed 0 = zeroBall := by40  rw [signRecursion_eq]41  simp [signRecursionStep]4243@[simp] theorem signRecursion_one (seed : UnitBall C(K, ℝ)) : signRecursion seed 1 = seed := by44  rw [signRecursion_eq]45  simp [signRecursionStep]4647def SignStageGood (seed : UnitBall C(K, ℝ)) (a : Ordinal.{u}) : Prop :=48  Disjoint (closure (signsPositiveBefore (signRecursion seed) a))49    (closure (signsNegativeBefore (signRecursion seed) a))5051theorem signRecursion_extension (seed : UnitBall C(K, ℝ)) (a : Ordinal.{u})52    (ha₀ : a ≠ 0) (ha₁ : a ≠ 1) (ha : SignStageGood seed a) :53    (∀ t ∈ closure (signsPositiveBefore (signRecursion seed) a), (signRecursion seed a).val t = 1) ∧54    (∀ t ∈ closure (signsNegativeBefore (signRecursion seed) a), (signRecursion seed a).val t = -1) := by55  have h := (exists_sign_extension (signsPositiveBefore (signRecursion seed) a)56    (signsNegativeBefore (signRecursion seed) a) ha).choose_spec57  unfold SignStageGood signsPositiveBefore signsNegativeBefore at ha58  rw [signRecursion_eq]59  simpa only [signRecursionStep, if_neg ha₀, if_neg ha₁, dif_pos ha,60    signsPositiveBefore, signsNegativeBefore] using h6162theorem signRecursion_positive_saturated (seed : UnitBall C(K, ℝ)) (a b : Ordinal.{u})63    (hab : a < b) (hb : SignStageGood seed b) (t : K)64    (ht : 0 < (signRecursion seed a).val t) : (signRecursion seed b).val t = 1 := by65  have hb₀ : b ≠ 0 := ne_of_gt (lt_of_le_of_lt bot_le hab)66  by_cases hb₁ : b = 167  · have ha₀ : a = 0 := by simpa only [hb₁, Ordinal.lt_one_iff_zero] using hab68    simp only [ha₀, signRecursion_zero, zeroBall, ContinuousMap.zero_apply] at ht69    exact (lt_irrefl _ ht).elim70  · apply (signRecursion_extension seed b hb₀ hb₁ hb).1 t71    apply subset_closure72    exact mem_iUnion.mpr ⟨⟨a, hab⟩, ht⟩7374theorem signRecursion_negative_saturated (seed : UnitBall C(K, ℝ)) (a b : Ordinal.{u})75    (hab : a < b) (hb : SignStageGood seed b) (t : K)76    (ht : (signRecursion seed a).val t < 0) : (signRecursion seed b).val t = -1 := by77  have hb₀ : b ≠ 0 := ne_of_gt (lt_of_le_of_lt bot_le hab)78  by_cases hb₁ : b = 179  · have ha₀ : a = 0 := by simpa only [hb₁, Ordinal.lt_one_iff_zero] using hab80    simp only [ha₀, signRecursion_zero, zeroBall, ContinuousMap.zero_apply] at ht81    exact (lt_irrefl _ ht).elim82  · apply (signRecursion_extension seed b hb₀ hb₁ hb).2 t83    apply subset_closure84    exact mem_iUnion.mpr ⟨⟨a, hab⟩, ht⟩8586@[simp] theorem signStageGood_zero (seed : UnitBall C(K, ℝ)) : SignStageGood seed 0 := by87  simp [SignStageGood, signsPositiveBefore, signsNegativeBefore]8889theorem signsPositiveBefore_succ (seed : UnitBall C(K, ℝ)) (a : Ordinal.{u})90    (ha : SignStageGood seed a) :91    signsPositiveBefore (signRecursion seed) (Order.succ a) =92      {t | 0 < (signRecursion seed a).val t} := by93  ext t94  simp only [signsPositiveBefore, mem_iUnion, Set.mem_ofPred_eq]95  constructor96  · rintro ⟨b, hb⟩97    have hba : b.val ≤ a := Order.lt_succ_iff.mp b.property98    rcases hba.eq_or_lt with heq | hlt99    · simpa only [heq] using hb100    · rw [signRecursion_positive_saturated seed b.val a hlt ha t hb]101      norm_num102  · intro ht103    exact ⟨⟨a, Order.lt_succ a⟩, ht⟩104105theorem signsNegativeBefore_succ (seed : UnitBall C(K, ℝ)) (a : Ordinal.{u})106    (ha : SignStageGood seed a) :107    signsNegativeBefore (signRecursion seed) (Order.succ a) =108      {t | (signRecursion seed a).val t < 0} := by109  ext t110  simp only [signsNegativeBefore, mem_iUnion, Set.mem_ofPred_eq]111  constructor112  · rintro ⟨b, hb⟩113    have hba : b.val ≤ a := Order.lt_succ_iff.mp b.property114    rcases hba.eq_or_lt with heq | hlt115    · simpa only [heq] using hb116    · rw [signRecursion_negative_saturated seed b.val a hlt ha t hb]117      norm_num118  · intro ht119    exact ⟨⟨a, Order.lt_succ a⟩, ht⟩120121theorem signStageGood_succ (hK : IsFSpace K) (seed : UnitBall C(K, ℝ)) (a : Ordinal.{u})122    (ha : SignStageGood seed a) : SignStageGood seed (Order.succ a) := by123  unfold SignStageGood124  rw [signsPositiveBefore_succ seed a ha, signsNegativeBefore_succ seed a ha]125  exact hK.disjoint_sign_closures _126127theorem signRecursion_at_points (seed : UnitBall C(K, ℝ)) (p q : K)128    (hp : seed.val p = 1) (hq : seed.val q = -1) (a : Ordinal.{u})129    (ha₁ : 1 ≤ a) (ha : SignStageGood seed a) :130    (signRecursion seed a).val p = 1 ∧ (signRecursion seed a).val q = -1 := by131  rcases ha₁.eq_or_lt with heq | hlt132  · simpa only [← heq, signRecursion_one] using And.intro hp hq133  · constructor134    · apply signRecursion_positive_saturated seed 1 a hlt ha p135      simp only [signRecursion_one, hp]136      norm_num137    · apply signRecursion_negative_saturated seed 1 a hlt ha q138      simp only [signRecursion_one, hq]139      norm_num140141end BFPP

SHA-256