Analysis.lean

1import BFPP.Deficits2import BFPP.TwoProfiles34/-! # The two-channel analysis map -/56namespace BFPP78set_option autoImplicit false910open Set1112universe u v w13variable {K : Type u} [TopologicalSpace K] [CompactSpace K]14variable {ι : Type v} {κ : Type w}15  [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]1617def continuousBallNeg (f : UnitBall C(K, ℝ)) : UnitBall C(K, ℝ) :=18  ⟨-f.val, by simpa only [norm_neg] using f.property⟩1920@[simp] theorem continuousBallNeg_apply (f : UnitBall C(K, ℝ)) (t : K) :21    (continuousBallNeg f).val t = -f.val t := rfl2223theorem continuousBallNeg_isometry : Isometry (continuousBallNeg : UnitBall C(K, ℝ) → _) := by24  apply Isometry.of_dist_eq25  intro f g26  change dist (-f.val) (-g.val) = dist f.val g.val27  exact dist_neg_neg _ _2829/-- The level-set data needed by analysis; no synthesis operator is assumed. -/30structure InseparableLevels (K : Type u) (ι : Type v) (κ : Type w)31    [TopologicalSpace K] [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ] where32  positive : ι → Set K33  negative : κ → Set K34  positive_mono : Monotone positive35  negative_mono : Monotone negative36  positive_bot : positive ⊥ = ∅37  negative_bot : negative ⊥ = ∅38  inseparable : (closure (⋃ i, positive i) ∩ closure (⋃ j, negative j)).Nonempty3940namespace InseparableLevels4142noncomputable def analyze (F : InseparableLevels K ι κ) (f : UnitBall C(K, ℝ)) :43    TwoProfile ι κ := by44  let a := analysisProfile F.positive F.positive_mono F.positive_bot f45  let b := analysisProfile F.negative F.negative_mono F.negative_bot (continuousBallNeg f)46  refine ⟨(a, b), ?_⟩47  obtain ⟨p, hp, hp'⟩ := F.inseparable48  have ha : 1 - f.val p ≤ a.tail :=49    analysisProfile_tail_at_closure _ _ _ _ p hp50  have hb : 1 + f.val p ≤ b.tail := by51    simpa only [continuousBallNeg_apply, sub_neg_eq_add] using52      analysisProfile_tail_at_closure F.negative F.negative_mono F.negative_bot53        (continuousBallNeg f) p hp'54  linarith5556@[simp] theorem analyze_positive (F : InseparableLevels K ι κ) (f : UnitBall C(K, ℝ)) (i : ι) :57    (F.analyze f).val.1.val i = deficit (F.positive i) f := rfl5859@[simp] theorem analyze_negative (F : InseparableLevels K ι κ) (f : UnitBall C(K, ℝ)) (j : κ) :60    (F.analyze f).val.2.val j = deficit (F.negative j) (continuousBallNeg f) := rfl6162theorem analyze_nonexpansive (F : InseparableLevels K ι κ) : LipschitzWith 1 F.analyze := by63  apply LipschitzWith.of_dist_le_mul64  intro f g65  simp only [NNReal.coe_one, one_mul]66  change max (dist (analysisProfile F.positive F.positive_mono F.positive_bot f)67    (analysisProfile F.positive F.positive_mono F.positive_bot g))68    (dist (analysisProfile F.negative F.negative_mono F.negative_bot (continuousBallNeg f))69      (analysisProfile F.negative F.negative_mono F.negative_bot (continuousBallNeg g))) ≤ dist f g70  apply max_le71  · simpa only [NNReal.coe_one, one_mul] using72      (analysisProfile_nonexpansive F.positive F.positive_mono F.positive_bot).dist_le_mul f g73  · have h := (analysisProfile_nonexpansive F.negative F.negative_mono F.negative_bot).dist_le_mul74      (continuousBallNeg f) (continuousBallNeg g)75    have hd : dist (continuousBallNeg f) (continuousBallNeg g) = dist f g :=76      dist_neg_neg f.val g.val77    simpa only [NNReal.coe_one, one_mul, hd] using h7879theorem analyze_le_of_bounds (F : InseparableLevels K ι κ) (f : UnitBall C(K, ℝ))80    (z : TwoProfile ι κ)81    (hp : ∀ i t, t ∈ F.positive i → 1 - z.val.1.val i ≤ f.val t)82    (hn : ∀ j t, t ∈ F.negative j → f.val t ≤ z.val.2.val j - 1) : F.analyze f ≤ z := by83  constructor84  · intro i85    apply deficit_le_of_pointwise _ _ _ (z.val.1.nonneg i)86    intro t ht87    have h := hp i t ht88    linarith89  · intro j90    apply deficit_le_of_pointwise _ _ _ (z.val.2.nonneg j)91    intro t ht92    simp only [continuousBallNeg_apply]93    have h := hn j t ht94    linarith9596/-- The synthesis construction must supply the map and the two level-set bounds. -/97theorem contractive_realization [NoMaxOrder ι] [NoMaxOrder κ]98    [WellFoundedLT ι] [WellFoundedLT κ]99    (F : InseparableLevels K ι κ) (J : TwoProfile ι κ → UnitBall C(K, ℝ))100    (hJ : LipschitzWith 1 J)101    (hp : ∀ z i t, t ∈ F.positive i → 1 - z.val.1.val i ≤ (J z).val t)102    (hn : ∀ z j t, t ∈ F.negative j → (J z).val t ≤ z.val.2.val j - 1) :103    LipschitzWith 1 (fun f => J ((F.analyze f).delay)) ∧104      ∀ f, J ((F.analyze f).delay) ≠ f :=105  BFPP.contractive_realization F.analyze J TwoProfile.delay F.analyze_nonexpansive hJ106    TwoProfile.delay_nonexpansive (fun z => F.analyze_le_of_bounds (J z) z (hp z) (hn z))107    TwoProfile.no_subsolution108109end InseparableLevels110end BFPP

SHA-256