MainTransfinite.lean

1import BFPP.RegularPairs2import BFPP.EncodedRecurrence34/-! # The main single-ordinal transfinite realization theorem -/56namespace BFPP78set_option autoImplicit false9open Set Order Cardinal1011universe u12variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [T2Space K]1314/-- An uncountable regular initial ordinal and all the actual realization maps.15No synthesis operator, inseparable pair, or fixed-point obstruction is assumed. -/16theorem exists_transfinite_realization (hF : IsFSpace K) (hED : ¬ ExtremallyDisconnected K) :17    ∃ κ : Ordinal.{u}, κ.card.ord = κ ∧ κ.card.IsRegular ∧ ℵ₀ < κ.card ∧18      ∃ D : Set (BoundedFamily (OrdinalIndex κ)),19        D.Nonempty ∧ IsClosed D ∧ Bornology.IsBounded D ∧ Convex ℝ D ∧20        ∃ (A : UnitBall C(K, ℝ) → D) (J : D → UnitBall C(K, ℝ)) (P : D → D),21          LipschitzWith 1 A ∧ LipschitzWith 1 J ∧ LipschitzWith 1 P ∧ IsTCP D P ∧22          (∀ z, A (J (P z)) ≠ z) ∧23          LipschitzWith 1 (fun f => J (P (A f))) ∧ (∀ f, J (P (A f)) ≠ f) := by24  obtain ⟨R⟩ := exists_regularOrdinalPair hF hED25  letI : Fact (IsSuccLimit R.positiveLength) := ⟨R.positiveLimit⟩26  letI : Fact (IsSuccLimit R.negativeLength) := ⟨R.negativeLimit⟩27  letI : Fact (IsSuccLimit R.length) := ⟨R.length_isLimit⟩28  have hp : R.positiveLength ≤ R.length := le_max_left _ _29  have hn : R.negativeLength ≤ R.length := le_max_right _ _30  refine ⟨R.length, R.length_isInitial, R.length_card_isRegular, R.length_uncountable hF,31    encodedSet hp hn, encodedSet_nonempty hp hn, encodedSet_isClosed hp hn,32    encodedSet_isBounded hp hn, encodedSet_convex hp hn,33    encodedAnalysis hp hn R.families, encodedSynthesis hp hn R.families,34    encodedPropagator hp hn, encodedAnalysis_nonexpansive hp hn R.families,35    encodedSynthesis_nonexpansive hp hn R.families, encodedPropagator_nonexpansive hp hn,36    encodedPropagator_isTCP hp hn, encoded_coefficient_fixedPointFree hp hn R.families, ?_, ?_⟩37  · exact nonexpansive_transfer _ _ _ (encodedAnalysis_nonexpansive hp hn R.families)38      (encodedSynthesis_nonexpansive hp hn R.families) (encodedPropagator_nonexpansive hp hn)39  · exact fixedPointFree_transfer _ _ _ (encoded_coefficient_fixedPointFree hp hn R.families)4041end BFPP

SHA-256