CenteredSynthesis.lean

1import BFPP.PositiveSynthesis23/-! # Sharp estimates for the centered synthesis channel45These proofs use positivity and uniform approximation. They do not require6representing measures to prove the contraction estimate.7-/89namespace BFPP1011set_option autoImplicit false1213open Set Order14open scoped ZeroAtInfty1516universe u v17variable {ι : Type u} [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]18  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]19variable {K : Type v} [TopologicalSpace K] [CompactSpace K]2021theorem centeredSynthesis_bounds (w : ι → C(K, ℝ))22    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)23    (a : Profile ι) (c : ℝ) (hc : 1 - a.tail ≤ c) (hc' : -1 ≤ c ∧ c ≤ 1) (t : K) :24    -1 ≤ c + synthesisOperator w (a.positiveTail c hc) t ∧25      c + synthesisOperator w (a.positiveTail c hc) t ≤ 1 := by26  have hpoint : ∀ i, -1 - c ≤ a.positiveTail c hc i ∧ a.positiveTail c hc i ≤ 1 - c := by27    intro i28    constructor29    · linarith [a.positiveTail_nonneg c hc i]30    · have h := a.positiveTail_le c hc i31      simpa only [max_eq_left (sub_nonneg.mpr hc'.2)] using h32  have h := synthesisOperator_preserves_bounds w hw hb stepCombination_denseRange33    (a.positiveTail c hc) (-1 - c) (1 - c) (by linarith [hc'.1])34    (by linarith [hc'.2]) hpoint t35  exact ⟨by linarith [h.1], by linarith [h.2]⟩3637theorem centeredSynthesis_dist (w : ι → C(K, ℝ))38    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)39    (a b : Profile ι) (c d : ℝ) (hc : 1 - a.tail ≤ c) (hd : 1 - b.tail ≤ d)40    (r : ℝ) (hab : dist a b ≤ r) (hcd : |c - d| ≤ r) (t : K) :41    |(c + synthesisOperator w (a.positiveTail c hc) t) -42      (d + synthesisOperator w (b.positiveTail d hd) t)| ≤ r := by43  let f : C₀(ι, ℝ) := a.positiveTail c hc - b.positiveTail d hd44  have hdelta := abs_le.mp hcd45  have hpoint : ∀ i, -r - (c - d) ≤ f i ∧ f i ≤ r - (c - d) := by46    intro i47    have h := abs_le.mp (Profile.center_add_positiveTail_dist a b c d hc hd r hab hcd i)48    change -r - (c - d) ≤ a.positiveTail c hc i - b.positiveTail d hd i ∧49      a.positiveTail c hc i - b.positiveTail d hd i ≤ r - (c - d)50    exact ⟨by linarith [h.1], by linarith [h.2]⟩51  have h := synthesisOperator_preserves_bounds w hw hb stepCombination_denseRange52    f (-r - (c - d)) (r - (c - d)) (by linarith [hdelta.1])53    (by linarith [hdelta.2]) hpoint t54  dsimp only [f] at h55  rw [map_sub] at h56  simp only [ContinuousMap.sub_apply] at h57  exact abs_le.mpr ⟨by linarith [h.1], by linarith [h.2]⟩5859theorem centeredSynthesis_at_level (w : ι → C(K, ℝ))60    (hw : ∀ t, Monotone (fun i => w i t)) (hb : ∀ i t, 0 ≤ w i t ∧ w i t ≤ 1)61    (a : Profile ι) (c : ℝ) (hc : 1 - a.tail ≤ c) (i : ι) (t : K) (ht : w i t = 1) :62    1 - a.val i ≤ c + synthesisOperator w (a.positiveTail c hc) t := by63  have hlocal : ∀ j, j ≤ i → 1 - a.val i - c ≤ a.positiveTail c hc j := by64    intro j hji65    have h₁ := a.regularizeValue_le_apply j66    have h₂ := a.monotone hji67    have h₃ : 1 - a.regularizeValue j - c ≤ a.positiveTail c hc j := le_max_left _ _68    linarith69  have h := synthesisOperator_lower_on_initialSegment w hw hb (a.positiveTail c hc)70    (a.positiveTail_nonneg c hc) i t ht (1 - a.val i - c) hlocal71  linarith7273end BFPP

SHA-256