ContinuousBall.lean

1import BFPP.Transfer2import Mathlib.Topology.ContinuousMap.Compact3import Mathlib.Topology.ContinuousMap.Algebra4import Mathlib.Tactic.FunProp5import Mathlib.Tactic.Linarith6import Mathlib.Tactic.Ring78/-! # The closed unit ball of real continuous functions -/910namespace BFPP1112set_option autoImplicit false1314universe u15variable {K : Type u} [TopologicalSpace K] [CompactSpace K]1617theorem continuousBall_abs_le (f : UnitBall C(K, ℝ)) (t : K) : |f.val t| ≤ 1 := by18  have h : |f.val t| ≤ ‖f.val‖ := by19    simpa only [Real.norm_eq_abs] using f.val.norm_coe_le_norm t20  exact h.trans f.property2122theorem continuousBall_bounds (f : UnitBall C(K, ℝ)) (t : K) :23    -1 ≤ f.val t ∧ f.val t ≤ 1 := abs_le.mp (continuousBall_abs_le f t)2425theorem continuousMap_abs_sub_le_dist (f g : C(K, ℝ)) (t : K) :26    |f t - g t| ≤ dist f g := by27  simpa only [Real.dist_eq] using ContinuousMap.dist_apply_le_dist (f := f) (g := g) t2829/-- The classical affine sign-extension map, on the whole closed unit ball. -/30noncomputable def signStep (h : C(K, ℝ)) (hh : ∀ t, |h t| ≤ 1)31    (f : UnitBall C(K, ℝ)) : UnitBall C(K, ℝ) := by32  let g : C(K, ℝ) := ⟨fun t => (1 - |h t|) * f.val t + h t, by fun_prop⟩33  refine ⟨g, (ContinuousMap.norm_le g (by norm_num)).2 ?_⟩34  intro t35  change |(1 - |h t|) * f.val t + h t| ≤ 136  have hp : 0 ≤ 1 - |h t| := sub_nonneg.mpr (hh t)37  calc38    |(1 - |h t|) * f.val t + h t| ≤ |(1 - |h t|) * f.val t| + |h t| :=39      abs_add_le _ _40    _ = (1 - |h t|) * |f.val t| + |h t| := by rw [abs_mul, abs_of_nonneg hp]41    _ ≤ (1 - |h t|) * 1 + |h t| :=42      add_le_add (mul_le_mul_of_nonneg_left (continuousBall_abs_le f t) hp) le_rfl43    _ = 1 := by ring4445@[simp] theorem signStep_apply (h : C(K, ℝ)) (hh : ∀ t, |h t| ≤ 1)46    (f : UnitBall C(K, ℝ)) (t : K) :47    (signStep h hh f).val t = (1 - |h t|) * f.val t + h t := rfl4849theorem signStep_nonexpansive (h : C(K, ℝ)) (hh : ∀ t, |h t| ≤ 1) :50    LipschitzWith 1 (signStep h hh) := by51  apply LipschitzWith.of_dist_le_mul52  intro f g53  simp only [NNReal.coe_one, one_mul]54  change dist (signStep h hh f).val (signStep h hh g).val ≤ dist f g55  apply (ContinuousMap.dist_le dist_nonneg).256  intro t57  rw [Real.dist_eq, signStep_apply, signStep_apply]58  have hp : 0 ≤ 1 - |h t| := sub_nonneg.mpr (hh t)59  have hp' : 1 - |h t| ≤ 1 := by linarith [abs_nonneg (h t)]60  calc61    |(1 - |h t|) * f.val t + h t - ((1 - |h t|) * g.val t + h t)| =62        |(1 - |h t|) * (f.val t - g.val t)| := by congr 1 <;> ring63    _ = (1 - |h t|) * |f.val t - g.val t| := by rw [abs_mul, abs_of_nonneg hp]64    _ ≤ 1 * |f.val t - g.val t| := mul_le_mul_of_nonneg_right hp' (abs_nonneg _)65    _ ≤ dist f g := by66      rw [one_mul]67      exact continuousMap_abs_sub_le_dist f.val g.val t6869theorem signStep_fixedPoint_positive (h : C(K, ℝ)) (hh : ∀ t, |h t| ≤ 1)70    (f : UnitBall C(K, ℝ)) (hf : signStep h hh f = f) (t : K) (ht : 0 < h t) :71    f.val t = 1 := by72  have he := congrArg (fun z : UnitBall C(K, ℝ) => z.val t) hf73  rw [signStep_apply, abs_of_pos ht] at he74  nlinarith7576theorem signStep_fixedPoint_negative (h : C(K, ℝ)) (hh : ∀ t, |h t| ≤ 1)77    (f : UnitBall C(K, ℝ)) (hf : signStep h hh f = f) (t : K) (ht : h t < 0) :78    f.val t = -1 := by79  have he := congrArg (fun z : UnitBall C(K, ℝ) => z.val t) hf80  rw [signStep_apply, abs_of_neg ht] at he81  nlinarith8283end BFPP

SHA-256