SaturatedChains.lean

1import BFPP.Families23/-! # Inseparable families obtained from saturated sign chains -/45namespace BFPP67set_option autoImplicit false89open Set1011universe u v12variable {K : Type u} {ι : Type v} [TopologicalSpace K] [CompactSpace K]13  [LinearOrder ι] [OrderBot ι]1415structure SaturatedSignChain (K : Type u) (ι : Type v)16    [TopologicalSpace K] [CompactSpace K] [LinearOrder ι] [OrderBot ι] where17  functions : ι → UnitBall C(K, ℝ)18  at_bot : (functions ⊥).val = 019  positive : ∀ i j, i < j → ∀ t, 0 < (functions i).val t → (functions j).val t = 120  negative : ∀ i j, i < j → ∀ t, (functions i).val t < 0 → (functions j).val t = -121  terminal : (closure (⋃ i, {t | 0 < (functions i).val t}) ∩22    closure (⋃ i, {t | (functions i).val t < 0})).Nonempty2324namespace SaturatedSignChain2526noncomputable def positivePart (H : SaturatedSignChain K ι) (i : ι) : C(K, ℝ) :=27  ⟨fun t => max ((H.functions i).val t) 0, (H.functions i).val.continuous.max continuous_const⟩2829noncomputable def negativePart (H : SaturatedSignChain K ι) (i : ι) : C(K, ℝ) :=30  ⟨fun t => max (-(H.functions i).val t) 0, (H.functions i).val.continuous.neg.max continuous_const⟩3132noncomputable def positiveFamily (H : SaturatedSignChain K ι) : IncreasingFamily K ι where33  functions := H.positivePart34  monotone t := by35    intro i j hij36    rcases hij.eq_or_lt with rfl | hij37    · exact le_rfl38    change max ((H.functions i).val t) 0 ≤ max ((H.functions j).val t) 039    by_cases hi : 0 < (H.functions i).val t40    · rw [H.positive i j hij t hi, max_eq_left (by norm_num : (0 : ℝ) ≤ 1)]41      exact max_le (continuousBall_bounds (H.functions i) t).2 (by norm_num)42    · rw [max_eq_right (le_of_not_gt hi)]43      exact le_max_right _ _44  bounds i t := ⟨le_max_right _ _,45    max_le (continuousBall_bounds (H.functions i) t).2 (by norm_num)⟩46  at_bot := by47    ext t48    change max ((H.functions ⊥).val t) 0 = 049    simp [H.at_bot]5051noncomputable def negativeFamily (H : SaturatedSignChain K ι) : IncreasingFamily K ι where52  functions := H.negativePart53  monotone t := by54    intro i j hij55    rcases hij.eq_or_lt with rfl | hij56    · exact le_rfl57    change max (-(H.functions i).val t) 0 ≤ max (-(H.functions j).val t) 058    by_cases hi : (H.functions i).val t < 059    · rw [H.negative i j hij t hi, neg_neg, max_eq_left (by norm_num : (0 : ℝ) ≤ 1)]60      have h := (continuousBall_bounds (H.functions i) t).161      exact max_le (by linarith) (by norm_num)62    · rw [max_eq_right (neg_nonpos.mpr (le_of_not_gt hi))]63      exact le_max_right _ _64  bounds i t := by65    refine ⟨le_max_right _ _, max_le ?_ (by norm_num)⟩66    have h := (continuousBall_bounds (H.functions i) t).167    linarith68  at_bot := by69    ext t70    change max (-(H.functions ⊥).val t) 0 = 071    simp [H.at_bot]7273theorem orthogonal_parts (H : SaturatedSignChain K ι) (i j : ι) (t : K) :74    H.positiveFamily.functions i t * H.negativeFamily.functions j t = 0 := by75  change max ((H.functions i).val t) 0 * max (-(H.functions j).val t) 0 = 076  by_cases hi : 0 < (H.functions i).val t77  · by_cases hj : (H.functions j).val t < 078    · exfalso79      rcases lt_trichotomy i j with hij | rfl | hji80      · have h := H.positive i j hij t hi81        linarith82      · linarith83      · have h := H.negative j i hji t hj84        linarith85    · rw [max_eq_right (neg_nonpos.mpr (le_of_not_gt hj)), mul_zero]86  · rw [max_eq_right (le_of_not_gt hi), zero_mul]8788theorem positive_union [NoMaxOrder ι] (H : SaturatedSignChain K ι) :89    (⋃ i, H.positiveFamily.levels i) = ⋃ i, {t | 0 < (H.functions i).val t} := by90  ext t91  simp only [mem_iUnion, IncreasingFamily.levels, Set.mem_ofPred_eq]92  constructor93  · rintro ⟨i, hi⟩94    refine ⟨i, ?_⟩95    change max ((H.functions i).val t) 0 = 1 at hi96    by_contra h97    rw [max_eq_right (le_of_not_gt h)] at hi98    norm_num at hi99  · rintro ⟨i, hi⟩100    obtain ⟨j, hij⟩ := exists_gt i101    refine ⟨j, ?_⟩102    change max ((H.functions j).val t) 0 = 1103    rw [H.positive i j hij t hi]104    norm_num105106theorem negative_union [NoMaxOrder ι] (H : SaturatedSignChain K ι) :107    (⋃ i, H.negativeFamily.levels i) = ⋃ i, {t | (H.functions i).val t < 0} := by108  ext t109  simp only [mem_iUnion, IncreasingFamily.levels, Set.mem_ofPred_eq]110  constructor111  · rintro ⟨i, hi⟩112    refine ⟨i, ?_⟩113    change max (-(H.functions i).val t) 0 = 1 at hi114    by_contra h115    rw [max_eq_right (neg_nonpos.mpr (le_of_not_gt h))] at hi116    norm_num at hi117  · rintro ⟨i, hi⟩118    obtain ⟨j, hij⟩ := exists_gt i119    refine ⟨j, ?_⟩120    change max (-(H.functions j).val t) 0 = 1121    rw [H.negative i j hij t hi]122    norm_num123124noncomputable def toInseparablePair [NoMaxOrder ι] (H : SaturatedSignChain K ι) :125    InseparablePair K ι ι where126  positive := H.positiveFamily127  negative := H.negativeFamily128  orthogonal := H.orthogonal_parts129  inseparable := by130    rw [H.positive_union, H.negative_union]131    exact H.terminal132133end SaturatedSignChain134end BFPP

SHA-256