C0Profiles.lean

1import BFPP.Regularization2import BFPP.Center3import Mathlib.Topology.ContinuousMap.ZeroAtInfty4import Mathlib.Topology.Order.Compact5import Mathlib.Topology.Order.MonotoneConvergence6import Mathlib.Tactic.FunProp78/-! # Synthesis profiles vanish at infinity -/910namespace BFPP1112set_option autoImplicit false1314open Set Order Filter Topology15open scoped ZeroAtInfty1617universe u18variable {ι : Type u} [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]19  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]2021namespace Profile2223theorem regularize_tendsto_tail (a : Profile ι) :24    Tendsto a.regularizeValue atTop (𝓝 a.tail) := by25  have h := tendsto_atTop_ciSup a.regularize.monotone a.regularize.val.bddAbove_range26  change Tendsto a.regularizeValue atTop (𝓝 a.regularize.tail) at h27  rwa [tail_regularize] at h2829/-- The positive-part profile used by the positive synthesis channel. -/30noncomputable def positiveTail (a : Profile ι) (c : ℝ) (hc : 1 - a.tail ≤ c) : C₀(ι, ℝ) where31  toFun i := max (1 - a.regularizeValue i - c) 032  continuous_toFun := ((continuous_const.sub a.regularizeValue_continuous).sub33    continuous_const).max continuous_const34  zero_at_infty' := by35    have h := (((tendsto_const_nhds (x := (1 : ℝ))).sub a.regularize_tendsto_tail).sub36      (tendsto_const_nhds (x := c))).max (tendsto_const_nhds (x := (0 : ℝ)))37    have hz : max (1 - a.tail - c) 0 = 0 := max_eq_right (by linarith)38    rw [hz] at h39    exact h.mono_left cocompact_le_atTop4041@[simp] theorem positiveTail_apply (a : Profile ι) (c : ℝ) (hc : 1 - a.tail ≤ c) (i : ι) :42    a.positiveTail c hc i = max (1 - a.regularizeValue i - c) 0 := rfl4344theorem positiveTail_nonneg (a : Profile ι) (c : ℝ) (hc : 1 - a.tail ≤ c) (i : ι) :45    0 ≤ a.positiveTail c hc i := le_max_right _ _4647theorem positiveTail_le (a : Profile ι) (c : ℝ) (hc : 1 - a.tail ≤ c) (i : ι) :48    a.positiveTail c hc i ≤ max (1 - c) 0 := by49  apply max_le_max _ le_rfl50  have h := a.regularizeValue_nonneg i51  linarith5253theorem center_add_positiveTail (a : Profile ι) (c : ℝ) (hc : 1 - a.tail ≤ c) (i : ι) :54    c + a.positiveTail c hc i = max c (1 - a.regularizeValue i) := by55  rw [positiveTail_apply]56  by_cases h : 0 ≤ 1 - a.regularizeValue i - c57  · rw [max_eq_left h, max_eq_right (by linarith)]58    ring59  · rw [max_eq_right (le_of_not_ge h), max_eq_left (by linarith)]60    ring6162/-- The center and the profile enter a single maximum, preserving constant one. -/63theorem center_add_positiveTail_dist (a b : Profile ι) (c d : ℝ)64    (hc : 1 - a.tail ≤ c) (hd : 1 - b.tail ≤ d) (r : ℝ)65    (hab : dist a b ≤ r) (hcd : |c - d| ≤ r) (i : ι) :66    |(c + a.positiveTail c hc i) - (d + b.positiveTail d hd i)| ≤ r := by67  rw [center_add_positiveTail, center_add_positiveTail]68  apply max_nonexpansive_bound hcd69  have h₁ := BoundedFamily.abs_sub_apply_le_dist a.regularize.val b.regularize.val i70  have h₂ := regularize_nonexpansive.dist_le_mul a b71  have h₂' : dist a.regularize b.regularize ≤ dist a b := by72    simpa only [NNReal.coe_one, one_mul] using h₂73  have h₃ : |a.regularizeValue i - b.regularizeValue i| ≤ r :=74    h₁.trans (h₂'.trans hab)75  calc76    |1 - a.regularizeValue i - (1 - b.regularizeValue i)| =77        |b.regularizeValue i - a.regularizeValue i| := by congr 1; ring78    _ = |a.regularizeValue i - b.regularizeValue i| := abs_sub_comm _ _79    _ ≤ r := h₃8081end Profile82end BFPP

SHA-256