BoundedFamilies.lean

1import BFPP.Suprema2import Mathlib.Topology.ContinuousMap.Bounded.Normed3import Mathlib.Topology.MetricSpace.Lipschitz45/-!6# Bounded families with their genuine supremum metric78The index is given the discrete topology only inside this abbreviation.9It can independently carry an order topology elsewhere in the construction.10-/1112namespace BFPP1314set_option autoImplicit false1516open Set1718universe u1920abbrev BoundedFamily (ι : Type u) :=21  @BoundedContinuousFunction ι ℝ ⊥ inferInstance2223namespace BoundedFamily2425variable {ι : Type u}2627noncomputable def ofBound (f : ι → ℝ) (M : ℝ) (h : ∀ i, ‖f i‖ ≤ M) :28    BoundedFamily ι := by29  letI : TopologicalSpace ι := ⊥30  letI : DiscreteTopology ι := ⟨rfl⟩31  exact {32    toFun := f33    continuous_toFun := continuous_of_discreteTopology34    map_bounded' := ⟨2 * M, fun i j => by35      calc36        dist (f i) (f j) ≤ ‖f i‖ + ‖f j‖ := dist_le_norm_add_norm _ _37        _ ≤ 2 * M := by linarith [h i, h j]⟩ }3839@[simp] theorem ofBound_apply (f : ι → ℝ) (M : ℝ) (h : ∀ i, ‖f i‖ ≤ M) (i : ι) :40    ofBound f M h i = f i := rfl4142theorem abs_apply_le_norm (f : BoundedFamily ι) (i : ι) : |f i| ≤ ‖f‖ := by43  letI : TopologicalSpace ι := ⊥44  simpa only [Real.norm_eq_abs] using BoundedContinuousFunction.norm_coe_le_norm f i4546theorem bddAbove_range (f : BoundedFamily ι) : BddAbove (range f) := by47  refine ⟨‖f‖, ?_⟩48  rintro _ ⟨i, rfl⟩49  exact (abs_le.mp (abs_apply_le_norm f i)).25051theorem bddBelow_range (f : BoundedFamily ι) : BddBelow (range f) := by52  refine ⟨-‖f‖, ?_⟩53  rintro _ ⟨i, rfl⟩54  exact (abs_le.mp (abs_apply_le_norm f i)).15556theorem abs_sub_apply_le_dist (f g : BoundedFamily ι) (i : ι) :57    |f i - g i| ≤ dist f g := by58  letI : TopologicalSpace ι := ⊥59  simpa only [Real.dist_eq] using60    BoundedContinuousFunction.dist_coe_le_dist (f := f) (g := g) i6162theorem dist_le_iff (f g : BoundedFamily ι) {d : ℝ} (hd : 0 ≤ d) :63    dist f g ≤ d ↔ ∀ i, |f i - g i| ≤ d := by64  letI : TopologicalSpace ι := ⊥65  simpa only [Real.dist_eq] using BoundedContinuousFunction.dist_le (f := f) (g := g) hd6667theorem evaluation_nonexpansive (i : ι) :68    LipschitzWith 1 (fun f : BoundedFamily ι => f i) := by69  apply LipschitzWith.of_dist_le_mul70  intro f g71  simpa only [NNReal.coe_one, one_mul, Real.dist_eq] using abs_sub_apply_le_dist f g i7273noncomputable def supremum (f : BoundedFamily ι) : ℝ := ⨆ i, f i7475noncomputable def infimum (f : BoundedFamily ι) : ℝ := ⨅ i, f i7677theorem supremum_nonexpansive [Nonempty ι] :78    LipschitzWith 1 (supremum : BoundedFamily ι → ℝ) := by79  apply LipschitzWith.of_dist_le_mul80  intro f g81  simpa only [NNReal.coe_one, one_mul, Real.dist_eq, supremum] using82    abs_ciSup_sub_ciSup_le f g f.bddAbove_range g.bddAbove_range (dist f g)83      (abs_sub_apply_le_dist f g)8485theorem infimum_nonexpansive [Nonempty ι] :86    LipschitzWith 1 (infimum : BoundedFamily ι → ℝ) := by87  apply LipschitzWith.of_dist_le_mul88  intro f g89  simpa only [NNReal.coe_one, one_mul, Real.dist_eq, infimum] using90    abs_ciInf_sub_ciInf_le f g f.bddBelow_range g.bddBelow_range (dist f g)91      (abs_sub_apply_le_dist f g)9293noncomputable def reindex {κ : Type*} (r : κ → ι) (f : BoundedFamily ι) :94    BoundedFamily κ := ofBound (fun j => f (r j)) ‖f‖95      (fun j => by simpa only [Real.norm_eq_abs] using abs_apply_le_norm f (r j))9697@[simp] theorem reindex_apply {κ : Type*} (r : κ → ι) (f : BoundedFamily ι) (j : κ) :98    reindex r f j = f (r j) := rfl99100theorem reindex_nonexpansive {κ : Type*} (r : κ → ι) :101    LipschitzWith 1 (reindex r : BoundedFamily ι → BoundedFamily κ) := by102  apply LipschitzWith.of_dist_le_mul103  intro f g104  simp only [NNReal.coe_one, one_mul]105  apply (dist_le_iff _ _ dist_nonneg).2106  intro j107  exact abs_sub_apply_le_dist f g (r j)108109end BoundedFamily110end BFPP

SHA-256