Realization.lean

1import BFPP.Families2import BFPP.TwoProfileGeometry34/-! # Realization on the whole closed unit ball from an inseparable pair -/56namespace BFPP78set_option autoImplicit false910open Set11open scoped ZeroAtInfty1213universe u v w14variable {K : Type u} {ι : Type v} {κ : Type w}15  [TopologicalSpace K] [CompactSpace K]16  [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]17  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]18  [LinearOrder κ] [OrderBot κ] [SuccOrder κ] [NoMaxOrder κ]19  [TopologicalSpace κ] [OrderTopology κ] [CompactIccSpace κ]2021namespace InseparablePair2223noncomputable def positiveInput (z : TwoProfile ι κ) : C₀(ι, ℝ) :=24  z.val.1.positiveTail z.center z.center_bounds.2.2.12526noncomputable def negativeInput (z : TwoProfile ι κ) : C₀(κ, ℝ) :=27  z.val.2.positiveTail (-z.center) (by have h := z.center_bounds.2.2.2; linarith)2829noncomputable def positiveOutput (F : InseparablePair K ι κ) (z : TwoProfile ι κ) : C(K, ℝ) :=30  synthesisOperator F.positive.functions (positiveInput z)3132noncomputable def negativeOutput (F : InseparablePair K ι κ) (z : TwoProfile ι κ) : C(K, ℝ) :=33  synthesisOperator F.negative.functions (negativeInput z)3435theorem positiveOutput_zero (F : InseparablePair K ι κ) (t : K)36    (ht : ∀ i, F.positive.functions i t = 0) (z : TwoProfile ι κ) : F.positiveOutput z t = 0 :=37  synthesisOperator_zero_at _ F.positive.monotone F.positive.bounds38    stepCombination_denseRange t ht _3940theorem negativeOutput_zero (F : InseparablePair K ι κ) (t : K)41    (ht : ∀ j, F.negative.functions j t = 0) (z : TwoProfile ι κ) : F.negativeOutput z t = 0 :=42  synthesisOperator_zero_at _ F.negative.monotone F.negative.bounds43    stepCombination_denseRange t ht _4445theorem positiveOutput_centered_bounds (F : InseparablePair K ι κ) (z : TwoProfile ι κ) (t : K) :46    -1 ≤ z.center + F.positiveOutput z t ∧ z.center + F.positiveOutput z t ≤ 1 :=47  centeredSynthesis_bounds _ F.positive.monotone F.positive.bounds z.val.1 z.center _48    ⟨z.center_bounds.1, z.center_bounds.2.1⟩ t4950theorem negativeOutput_centered_bounds (F : InseparablePair K ι κ) (z : TwoProfile ι κ) (t : K) :51    -1 ≤ -z.center + F.negativeOutput z t ∧ -z.center + F.negativeOutput z t ≤ 1 := by52  apply centeredSynthesis_bounds _ F.negative.monotone F.negative.bounds z.val.2 (-z.center) _ _ t53  have h := z.center_bounds54  exact ⟨by linarith [h.2.1], by linarith [h.1]⟩5556noncomputable def synthesizeMap (F : InseparablePair K ι κ) (z : TwoProfile ι κ) : C(K, ℝ) :=57  ContinuousMap.const K z.center + F.positiveOutput z - F.negativeOutput z5859@[simp] theorem synthesizeMap_apply (F : InseparablePair K ι κ) (z : TwoProfile ι κ) (t : K) :60    F.synthesizeMap z t = z.center + F.positiveOutput z t - F.negativeOutput z t := rfl6162theorem synthesizeMap_bounds (F : InseparablePair K ι κ) (z : TwoProfile ι κ) (t : K) :63    -1 ≤ F.synthesizeMap z t ∧ F.synthesizeMap z t ≤ 1 := by64  rw [synthesizeMap_apply]65  rcases F.disjoint_channels t with hp | hn66  · rw [F.positiveOutput_zero t hp z]67    have h := F.negativeOutput_centered_bounds z t68    exact ⟨by linarith [h.2], by linarith [h.1]⟩69  · rw [F.negativeOutput_zero t hn z, sub_zero]70    exact F.positiveOutput_centered_bounds z t7172noncomputable def synthesize (F : InseparablePair K ι κ) (z : TwoProfile ι κ) :73    UnitBall C(K, ℝ) :=74  ⟨F.synthesizeMap z, (ContinuousMap.norm_le _ (by norm_num)).mpr75    (fun t => abs_le.mpr (F.synthesizeMap_bounds z t))⟩7677theorem positiveOutput_centered_dist (F : InseparablePair K ι κ) (z z' : TwoProfile ι κ) (t : K) :78    |(z.center + F.positiveOutput z t) - (z'.center + F.positiveOutput z' t)| ≤ dist z z' := by79  have hcenter : |z.center - z'.center| ≤ dist z z' := by80    simpa only [NNReal.coe_one, one_mul, Real.dist_eq] using81      TwoProfile.center_nonexpansive.dist_le_mul z z'82  exact centeredSynthesis_dist _ F.positive.monotone F.positive.bounds z.val.1 z'.val.183    z.center z'.center _ _ (dist z z') (le_max_left _ _) hcenter t8485theorem negativeOutput_centered_dist (F : InseparablePair K ι κ) (z z' : TwoProfile ι κ) (t : K) :86    |(-z.center + F.negativeOutput z t) - (-z'.center + F.negativeOutput z' t)| ≤ dist z z' := by87  have hcenter : |z.center - z'.center| ≤ dist z z' := by88    simpa only [NNReal.coe_one, one_mul, Real.dist_eq] using89      TwoProfile.center_nonexpansive.dist_le_mul z z'90  have hneg : |-z.center - (-z'.center)| ≤ dist z z' := by91    simpa only [neg_sub_neg, abs_sub_comm] using hcenter92  exact centeredSynthesis_dist _ F.negative.monotone F.negative.bounds z.val.2 z'.val.293    (-z.center) (-z'.center) _ _ (dist z z') (le_max_right _ _) hneg t9495theorem synthesize_nonexpansive (F : InseparablePair K ι κ) : LipschitzWith 1 F.synthesize := by96  apply LipschitzWith.of_dist_le_mul97  intro z z'98  simp only [NNReal.coe_one, one_mul]99  change dist (F.synthesizeMap z) (F.synthesizeMap z') ≤ dist z z'100  apply (ContinuousMap.dist_le dist_nonneg).mpr101  intro t102  rw [Real.dist_eq, synthesizeMap_apply, synthesizeMap_apply]103  rcases F.disjoint_channels t with hp | hn104  · rw [F.positiveOutput_zero t hp z, F.positiveOutput_zero t hp z']105    have h := abs_le.mp (F.negativeOutput_centered_dist z z' t)106    exact abs_le.mpr ⟨by linarith [h.2], by linarith [h.1]⟩107  · rw [F.negativeOutput_zero t hn z, F.negativeOutput_zero t hn z', sub_zero, sub_zero]108    exact F.positiveOutput_centered_dist z z' t109110theorem synthesize_at_positive_level (F : InseparablePair K ι κ) (z : TwoProfile ι κ)111    (i : ι) (t : K) (ht : t ∈ F.positive.levels i) :112    1 - z.val.1.val i ≤ (F.synthesize z).val t := by113  change 1 - z.val.1.val i ≤ F.synthesizeMap z t114  rw [synthesizeMap_apply, F.negativeOutput_zero t (F.negative_zero_at_positive_level i t ht) z,115    sub_zero]116  exact centeredSynthesis_at_level _ F.positive.monotone F.positive.bounds z.val.1117    z.center _ i t ht118119theorem synthesize_at_negative_level (F : InseparablePair K ι κ) (z : TwoProfile ι κ)120    (j : κ) (t : K) (ht : t ∈ F.negative.levels j) :121    (F.synthesize z).val t ≤ z.val.2.val j - 1 := by122  change F.synthesizeMap z t ≤ z.val.2.val j - 1123  rw [synthesizeMap_apply, F.positiveOutput_zero t (F.positive_zero_at_negative_level j t ht) z]124  have h := centeredSynthesis_at_level F.negative.functions F.negative.monotone F.negative.bounds125    z.val.2 (-z.center) (by have hc := z.center_bounds.2.2.2; linarith) j t ht126  change 1 - z.val.2.val j ≤ -z.center + F.negativeOutput z t at h127  linarith128129theorem analyze_synthesize_le (F : InseparablePair K ι κ) (z : TwoProfile ι κ) :130    F.levels.analyze (F.synthesize z) ≤ z :=131  F.levels.analyze_le_of_bounds (F.synthesize z) z (F.synthesize_at_positive_level z)132    (F.synthesize_at_negative_level z)133134/-- The final map for an already constructed inseparable pair. -/135noncomputable def ballMap (F : InseparablePair K ι κ) : UnitBall C(K, ℝ) → UnitBall C(K, ℝ) :=136  fun f => F.synthesize (F.levels.analyze f).delay137138theorem ballMap_nonexpansive (F : InseparablePair K ι κ) : LipschitzWith 1 F.ballMap :=139  nonexpansive_transfer F.levels.analyze F.synthesize TwoProfile.delay140    F.levels.analyze_nonexpansive F.synthesize_nonexpansive TwoProfile.delay_nonexpansive141142theorem ballMap_fixedPointFree [WellFoundedLT ι] [WellFoundedLT κ]143    (F : InseparablePair K ι κ) (f : UnitBall C(K, ℝ)) : F.ballMap f ≠ f :=144  fixedPointFree_of_order_domination F.levels.analyze F.synthesize TwoProfile.delay145    F.analyze_synthesize_le TwoProfile.no_subsolution f146147theorem not_hasBFPP [WellFoundedLT ι] [WellFoundedLT κ]148    (F : InseparablePair K ι κ) : ¬ HasBFPP C(K, ℝ) :=149  not_hasBFPP_of_fixedPointFree F.ballMap F.ballMap_nonexpansive F.ballMap_fixedPointFree150151end InseparablePair152end BFPP

SHA-256