Families.lean

1import BFPP.Analysis2import BFPP.CenteredSynthesis34/-! # Increasing families and their level sets -/56namespace BFPP78set_option autoImplicit false910open Set1112universe u v w1314structure IncreasingFamily (K : Type u) (ι : Type v)15    [TopologicalSpace K] [LinearOrder ι] [OrderBot ι] where16  functions : ι → C(K, ℝ)17  monotone : ∀ t, Monotone (fun i => functions i t)18  bounds : ∀ i t, 0 ≤ functions i t ∧ functions i t ≤ 119  at_bot : functions ⊥ = 02021namespace IncreasingFamily2223variable {K : Type u} {ι : Type v} [TopologicalSpace K] [LinearOrder ι] [OrderBot ι]2425def levels (F : IncreasingFamily K ι) (i : ι) : Set K := {t | F.functions i t = 1}2627theorem levels_monotone (F : IncreasingFamily K ι) : Monotone F.levels := by28  intro i j hij t ht29  have hm := F.monotone t hij30  have hb := (F.bounds j t).231  change F.functions i t = 1 at ht32  change F.functions j t = 133  linarith3435@[simp] theorem levels_bot (F : IncreasingFamily K ι) : F.levels ⊥ = ∅ := by36  ext t37  simp [levels, F.at_bot]3839end IncreasingFamily4041structure InseparablePair (K : Type u) (ι : Type v) (κ : Type w)42    [TopologicalSpace K] [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ] where43  positive : IncreasingFamily K ι44  negative : IncreasingFamily K κ45  orthogonal : ∀ i j t, positive.functions i t * negative.functions j t = 046  inseparable : (closure (⋃ i, positive.levels i) ∩ closure (⋃ j, negative.levels j)).Nonempty4748namespace InseparablePair4950variable {K : Type u} {ι : Type v} {κ : Type w}51  [TopologicalSpace K] [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]5253def levels (F : InseparablePair K ι κ) : InseparableLevels K ι κ where54  positive := F.positive.levels55  negative := F.negative.levels56  positive_mono := F.positive.levels_monotone57  negative_mono := F.negative.levels_monotone58  positive_bot := F.positive.levels_bot59  negative_bot := F.negative.levels_bot60  inseparable := F.inseparable6162theorem disjoint_channels (F : InseparablePair K ι κ) (t : K) :63    (∀ i, F.positive.functions i t = 0) ∨ (∀ j, F.negative.functions j t = 0) := by64  classical65  by_cases h : ∀ i, F.positive.functions i t = 066  · exact Or.inl h67  · right68    obtain ⟨i, hi⟩ := not_forall.mp h69    intro j70    exact (mul_eq_zero.mp (F.orthogonal i j t)).resolve_left hi7172theorem negative_zero_at_positive_level (F : InseparablePair K ι κ) (i : ι) (t : K)73    (ht : t ∈ F.positive.levels i) : ∀ j, F.negative.functions j t = 0 := by74  intro j75  have h := F.orthogonal i j t76  change F.positive.functions i t = 1 at ht77  simpa only [ht, one_mul] using h7879theorem positive_zero_at_negative_level (F : InseparablePair K ι κ) (j : κ) (t : K)80    (ht : t ∈ F.negative.levels j) : ∀ i, F.positive.functions i t = 0 := by81  intro i82  have h := F.orthogonal i j t83  change F.negative.functions j t = 1 at ht84  simpa only [ht, mul_one] using h8586end InseparablePair87end BFPP

SHA-256