FSpaceNecessary.lean

1import BFPP.ContinuousBall23/-! # BFPP implies the F-space property45The definition uses the standard separation characterization: disjoint cozero6sets of real continuous functions have disjoint closures.7-/89namespace BFPP1011set_option autoImplicit false1213open Set1415universe u1617def IsFSpace (K : Type u) [TopologicalSpace K] : Prop :=18  ∀ f g : C(K, ℝ), Disjoint {t | f t ≠ 0} {t | g t ≠ 0} →19    Disjoint (closure {t | f t ≠ 0}) (closure {t | g t ≠ 0})2021variable {K : Type u} [TopologicalSpace K] [CompactSpace K]2223theorem continuous_sign_of_hasBFPP (hB : HasBFPP C(K, ℝ)) (h : C(K, ℝ)) :24    ∃ s : UnitBall C(K, ℝ),25      (∀ t, 0 < h t → s.val t = 1) ∧ (∀ t, h t < 0 → s.val t = -1) := by26  let M : ℝ := max 1 ‖h‖27  have hM : 0 < M := lt_of_lt_of_le (by norm_num) (le_max_left _ _)28  let hn : C(K, ℝ) := ⟨fun t => h t / M, h.continuous.div_const M⟩29  have hhn : ∀ t, |hn t| ≤ 1 := by30    intro t31    change |h t / M| ≤ 132    rw [abs_div, abs_of_pos hM, div_le_one hM]33    have ht : |h t| ≤ ‖h‖ := by34      simpa only [Real.norm_eq_abs] using h.norm_coe_le_norm t35    exact ht.trans (le_max_right _ _)36  obtain ⟨s, hs⟩ := hB (signStep hn hhn) (signStep_nonexpansive hn hhn)37  refine ⟨s, ?_, ?_⟩38  · intro t ht39    exact signStep_fixedPoint_positive hn hhn s hs t (div_pos ht hM)40  · intro t ht41    exact signStep_fixedPoint_negative hn hhn s hs t (div_neg_of_neg_of_pos ht hM)4243theorem isFSpace_of_hasBFPP (hB : HasBFPP C(K, ℝ)) : IsFSpace K := by44  intro f g hfg45  let h : C(K, ℝ) := ⟨fun t => |f t| - |g t|, by fun_prop⟩46  obtain ⟨s, hsp, hsn⟩ := continuous_sign_of_hasBFPP hB h47  have hfsub : {t | f t ≠ 0} ⊆ {t | s.val t = 1} := by48    intro t ht49    have hg : g t = 0 := by50      by_contra hg51      exact Set.disjoint_left.mp hfg ht hg52    apply hsp t53    change 0 < |f t| - |g t|54    simpa only [hg, abs_zero, sub_zero] using abs_pos.mpr ht55  have hgsub : {t | g t ≠ 0} ⊆ {t | s.val t = -1} := by56    intro t ht57    have hf : f t = 0 := by58      by_contra hf59      exact Set.disjoint_left.mp hfg hf ht60    apply hsn t61    change |f t| - |g t| < 062    simpa only [hf, abs_zero, zero_sub, neg_lt_zero] using abs_pos.mpr ht63  have hfclosed : IsClosed {t | s.val t = 1} :=64    isClosed_eq s.val.continuous continuous_const65  have hgclosed : IsClosed {t | s.val t = -1} :=66    isClosed_eq s.val.continuous continuous_const67  apply Set.disjoint_left.mpr68  intro t ht ht'69  have hp : s.val t = 1 := closure_minimal hfsub hfclosed ht70  have hn : s.val t = -1 := closure_minimal hgsub hgclosed ht'71  linarith7273end BFPP

SHA-256