SignRealization.lean

1import BFPP.SignTermination2import BFPP.SaturatedChains3import BFPP.OrdinalIndex4import Mathlib.Topology.Connected.TotallyDisconnected56/-! # Realization of a stopped transfinite sign recursion -/78namespace BFPP910set_option autoImplicit false1112open Set Order TopologicalSpace1314universe u15variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [NormalSpace K]1617noncomputable def stoppedSignChain (seed : UnitBall C(K, ℝ)) (d : Ordinal.{u})18    [Fact (IsSuccLimit d)] (hd : ¬ SignStageGood seed d)19    (hbefore : ∀ a, a < d → SignStageGood seed a) :20    SaturatedSignChain K (OrdinalIndex d) where21  functions i := signRecursion seed i.val22  at_bot := by23    change (signRecursion seed 0).val = 024    rw [signRecursion_zero]25    rfl26  positive i j hij t ht :=27    signRecursion_positive_saturated seed i.val j.val hij (hbefore j.val j.property) t ht28  negative i j hij t ht :=29    signRecursion_negative_saturated seed i.val j.val hij (hbefore j.val j.property) t ht30  terminal := by31    change (closure (signsPositiveBefore (signRecursion seed) d) ∩32      closure (signsNegativeBefore (signRecursion seed) d)).Nonempty33    exact Set.not_disjoint_iff.mp hd3435theorem not_hasBFPP_of_clopenInseparable (hK : IsFSpace K)36    (seed : UnitBall C(K, ℝ)) (p q : K) (hpq : ClopenInseparable p q)37    (hp : seed.val p = 1) (hq : seed.val q = -1) : ¬ HasBFPP C(K, ℝ) := by38  obtain ⟨d, hlimit, hd, hbefore⟩ := exists_first_bad_limit hK seed p q hpq hp hq39  letI : Fact (IsSuccLimit d) := ⟨hlimit⟩40  exact (stoppedSignChain seed d hd hbefore).toInseparablePair.not_hasBFPP4142theorem exists_clopenInseparable_of_not_totallySeparated43    (hK : ¬ TotallySeparatedSpace K) : ∃ p q : K, p ≠ q ∧ ClopenInseparable p q := by44  classical45  by_contra hnone46  apply hK47  apply totallySeparatedSpace_iff_exists_isClopen.mpr48  intro p q hpq49  have hsep : ¬ ClopenInseparable p q := by50    intro h51    exact hnone ⟨p, q, hpq, h⟩52  unfold ClopenInseparable at hsep53  push_neg at hsep54  obtain ⟨s, hp, hq⟩ := hsep55  exact ⟨s, s.isClopen, hp, hq⟩5657theorem not_hasBFPP_of_not_totallySeparated [T2Space K] (hF : IsFSpace K)58    (hK : ¬ TotallySeparatedSpace K) : ¬ HasBFPP C(K, ℝ) := by59  obtain ⟨p, q, hpq, hinsep⟩ := exists_clopenInseparable_of_not_totallySeparated hK60  have hd : Disjoint (closure ({p} : Set K)) (closure ({q} : Set K)) := by61    simpa only [isClosed_singleton.closure_eq, disjoint_singleton] using hpq62  obtain ⟨seed, hp, hq⟩ := exists_sign_extension ({p} : Set K) {q} hd63  exact not_hasBFPP_of_clopenInseparable hF seed p q hinsep64    (hp p (subset_closure (mem_singleton p))) (hq q (subset_closure (mem_singleton q)))6566theorem totallySeparated_of_hasBFPP [T2Space K] (h : HasBFPP C(K, ℝ)) :67    TotallySeparatedSpace K := by68  by_contra hn69  exact not_hasBFPP_of_not_totallySeparated (isFSpace_of_hasBFPP h) hn h7071end BFPP

SHA-256