DiscretePropagation.lean

1import BFPP.Transfer2import Mathlib.Analysis.Normed.Module.Basic3import Mathlib.Tactic45/-! # The discrete affine propagation estimate in the introduction -/67namespace BFPP89set_option autoImplicit false1011variable {X E : Type*} [PseudoMetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E]1213/-- Coefficients and the translation are fixed independently of the input. -/14theorem affine_propagation_lipschitz (f g : X → E) (A B : NNReal)15    (hf : LipschitzWith A f) (hg : LipschitzWith B g) (a b : ℝ) (c : E) :16    LipschitzWith (‖a‖₊ * A + ‖b‖₊ * B) (fun x => a • f x + b • g x + c) := by17  apply LipschitzWith.of_dist_le_mul18  intro x y19  have hf' := hf.dist_le_mul x y20  have hg' := hg.dist_le_mul x y21  simp only [NNReal.coe_add, NNReal.coe_mul, coe_nnnorm]22  calc23    dist (a • f x + b • g x + c) (a • f y + b • g y + c) =24        dist (a • f x + b • g x) (a • f y + b • g y) := dist_add_right _ _ _25    _ ≤ dist (a • f x) (a • f y) + dist (b • g x) (b • g y) := dist_add_add_le _ _ _ _26    _ = ‖a‖ * dist (f x) (f y) + ‖b‖ * dist (g x) (g y) := by rw [dist_smul₀, dist_smul₀]27    _ ≤ ‖a‖ * (A * dist x y) + ‖b‖ * (B * dist x y) :=28      add_le_add (mul_le_mul_of_nonneg_left hf' (norm_nonneg _))29        (mul_le_mul_of_nonneg_left hg' (norm_nonneg _))30    _ = (‖a‖ * A + ‖b‖ * B) * dist x y := by ring3132theorem affine_propagation_nonexpansive (f g : X → E)33    (hf : LipschitzWith 1 f) (hg : LipschitzWith 1 g) (a b : ℝ) (c : E)34    (hab : |a| + |b| ≤ 1) : LipschitzWith 1 (fun x => a • f x + b • g x + c) := by35  apply (affine_propagation_lipschitz f g 1 1 hf hg a b c).weaken36  exact_mod_cast (by simpa only [Real.norm_eq_abs, mul_one] using hab :37    ‖a‖ * (1 : ℝ) + ‖b‖ * 1 ≤ 1)3839/-- The estimate at every step of the displayed discrete recurrence. -/40theorem discrete_recurrence_nonexpansive (S g : ℕ → X → E) (a b : ℕ → ℝ) (c : ℕ → E)41    (hrec : ∀ n x, S (n + 1) x = a n • S n x + b n • g n x + c n)42    (hzero : LipschitzWith 1 (S 0)) (hg : ∀ n, LipschitzWith 1 (g n))43    (hab : ∀ n, |a n| + |b n| ≤ 1) : ∀ n, LipschitzWith 1 (S n) := by44  intro n45  induction n with46  | zero => exact hzero47  | succ n ih =>48    have he : S (n + 1) = fun x => a n • S n x + b n • g n x + c n := funext (hrec n)49    rw [he]50    exact affine_propagation_nonexpansive (S n) (g n) ih (hg n) (a n) (b n) (c n) (hab n)5152end BFPP

SHA-256