NormalizedAppendix.lean

1import BFPP.TerminalNormalization23/-! # The appendix construction with terminal supremum norm one -/45namespace BFPP67set_option autoImplicit false8open Set Order Cardinal unitInterval910universe u v11variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [T2Space K]1213theorem unitInterval_coe_iSup {ι : Type v} [Nonempty ι] (f : ι → I) :14    ((⨆ i, f i : I) : ℝ) = ⨆ i, (f i : ℝ) :=15  Set.Icc.coe_iSup (by norm_num)1617theorem exists_normalized_terminal_supremum (hK : ¬ ExtremallyDisconnected K) :18    ∃ η : Cardinal.{u}, ℵ₀ ≤ η ∧ ∃ hη : IsSuccLimit η.ord,19      ∃ (s : OrdinalIndex η.ord → C(K, ℝ)) (sstar : BoundedFamily K),20        Monotone (fun i t => s i t) ∧ s ⟨0, hη.pos⟩ = 0 ∧21        (∀ i t, 0 ≤ s i t ∧ s i t ≤ 1) ∧22        (∀ i : OrdinalIndex η.ord, IsSuccLimit i.val → ∀ t,23          s i t = ⨆ j : Iio i, s j.val t) ∧24        (∀ t, sstar t = ⨆ i, s i t) ∧ (∀ t, 0 ≤ sstar t ∧ sstar t ≤ 1) ∧25        ‖sstar‖ = 1 ∧ ¬ Continuous (fun t => sstar t) := by26  obtain ⟨η, hinf, hη, s, f, hmono, hzero, hlim, hterminal, hdisc⟩ :=27    exists_terminal_pointwise_supremum_of_not_ED hK28  letI : Fact (IsSuccLimit η.ord) := ⟨hη⟩29  let a : ℝ := ‖boundedUnitFunction f‖⁻¹30  have ha : 0 < a := inv_pos.mpr (terminal_norm_pos f hdisc)31  let sn : OrdinalIndex η.ord → C(K, ℝ) := fun i =>32    ⟨fun t => a * (s i t : ℝ), normalized_profile_continuous f (s i)⟩33  have hsle : ∀ i t, s i t ≤ f t := by34    intro i t35    rw [hterminal t]36    exact le_iSup (fun j => s j t) i37  have hbdd : ∀ t, BddAbove (range (fun i => (s i t : ℝ))) := by38    intro t39    exact ⟨1, fun _ ⟨i, hi⟩ => hi ▸ (s i t).property.2⟩40  refine ⟨η, hinf, hη, sn, normalizedTerminal f, ?_, ?_, ?_, ?_, ?_,41    normalizedTerminal_bounds f hdisc, normalizedTerminal_norm f hdisc,42    normalizedTerminal_not_continuous f hdisc⟩43  · intro i j hij t44    change a * (s i t : ℝ) ≤ a * (s j t : ℝ)45    exact mul_le_mul_of_nonneg_left (hmono hij t) ha.le46  · apply ContinuousMap.ext47    intro t48    change a * (s ⟨0, hη.pos⟩ t : ℝ) = 049    rw [hzero]50    simp51  · intro i t52    exact normalized_profile_bounds f hdisc (s i) (hsle i) t53  · intro i hi t54    letI : Nonempty (Iio i) := ⟨⟨⟨0, hη.pos⟩, hi.pos⟩⟩55    have he : (s i t : ℝ) = ⨆ j : Iio i, (s j.val t : ℝ) := by56      rw [hlim i hi t]57      exact unitInterval_coe_iSup _58    change a * (s i t : ℝ) = ⨆ j : Iio i, a * (s j.val t : ℝ)59    rw [he]60    apply positive_scale_ciSup a ha61    exact ⟨1, fun _ ⟨j, hj⟩ => hj ▸ (s j.val t).property.2⟩62  · intro t63    have he : (f t : ℝ) = ⨆ i, (s i t : ℝ) := by64      rw [hterminal t]65      exact unitInterval_coe_iSup _66    change a * (f t : ℝ) = ⨆ i, a * (s i t : ℝ)67    rw [he]68    exact positive_scale_ciSup a ha _ (hbdd t)6970end BFPP

SHA-256