Envelopes.lean

1import BFPP.BoundedFamilies23/-!4# Upper and lower ordinal envelopes56The metric proof works on any nonempty preorder. Instantiating the index type7with the ordinals below a nonzero limit gives precisely Section 2.1 of the paper.8-/910namespace BFPP1112set_option autoImplicit false1314open Set1516universe u17variable {ι : Type u} [Preorder ι]1819noncomputable def upperTail (f : BoundedFamily ι) (b : ι) : ℝ :=20  BoundedFamily.supremum (BoundedFamily.reindex (fun j : Ici b => j.val) f)2122noncomputable def lowerTail (f : BoundedFamily ι) (b : ι) : ℝ :=23  BoundedFamily.infimum (BoundedFamily.reindex (fun j : Ici b => j.val) f)2425theorem abs_upperTail_le (f : BoundedFamily ι) (b : ι) : |upperTail f b| ≤ ‖f‖ := by26  letI : Nonempty (Ici b) := ⟨⟨b, le_rfl⟩⟩27  apply abs_le.mpr28  constructor29  · calc30      -‖f‖ ≤ f b := (abs_le.mp (f.abs_apply_le_norm b)).131      _ ≤ upperTail f b :=32        le_ciSup (BoundedFamily.bddAbove_range33          (BoundedFamily.reindex (fun j : Ici b => j.val) f)) ⟨b, le_rfl⟩34  · apply ciSup_le35    intro j36    exact (abs_le.mp (f.abs_apply_le_norm j.val)).23738theorem abs_lowerTail_le (f : BoundedFamily ι) (b : ι) : |lowerTail f b| ≤ ‖f‖ := by39  letI : Nonempty (Ici b) := ⟨⟨b, le_rfl⟩⟩40  apply abs_le.mpr41  constructor42  · apply le_ciInf43    intro j44    exact (abs_le.mp (f.abs_apply_le_norm j.val)).145  · calc46      lowerTail f b ≤ f b :=47        ciInf_le (BoundedFamily.bddBelow_range48          (BoundedFamily.reindex (fun j : Ici b => j.val) f)) ⟨b, le_rfl⟩49      _ ≤ ‖f‖ := (abs_le.mp (f.abs_apply_le_norm b)).25051noncomputable def upperTails (f : BoundedFamily ι) : BoundedFamily ι :=52  BoundedFamily.ofBound (upperTail f) ‖f‖ (abs_upperTail_le f)5354noncomputable def lowerTails (f : BoundedFamily ι) : BoundedFamily ι :=55  BoundedFamily.ofBound (lowerTail f) ‖f‖ (abs_lowerTail_le f)5657theorem upperTails_nonexpansive : LipschitzWith 1 (upperTails : BoundedFamily ι → _) := by58  apply LipschitzWith.of_dist_le_mul59  intro f g60  simp only [NNReal.coe_one, one_mul]61  apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).262  intro b63  letI : Nonempty (Ici b) := ⟨⟨b, le_rfl⟩⟩64  have h := (BoundedFamily.supremum_nonexpansive.comp65    (BoundedFamily.reindex_nonexpansive (fun j : Ici b => j.val))).dist_le_mul f g66  simpa only [NNReal.coe_mul, NNReal.coe_one, mul_one, one_mul,67    Real.dist_eq, upperTails, BoundedFamily.ofBound_apply, upperTail,68    Function.comp_def] using h6970theorem lowerTails_nonexpansive : LipschitzWith 1 (lowerTails : BoundedFamily ι → _) := by71  apply LipschitzWith.of_dist_le_mul72  intro f g73  simp only [NNReal.coe_one, one_mul]74  apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).275  intro b76  letI : Nonempty (Ici b) := ⟨⟨b, le_rfl⟩⟩77  have h := (BoundedFamily.infimum_nonexpansive.comp78    (BoundedFamily.reindex_nonexpansive (fun j : Ici b => j.val))).dist_le_mul f g79  simpa only [NNReal.coe_mul, NNReal.coe_one, mul_one, one_mul,80    Real.dist_eq, lowerTails, BoundedFamily.ofBound_apply, lowerTail,81    Function.comp_def] using h8283noncomputable def upperEnvelope (f : BoundedFamily ι) : ℝ :=84  BoundedFamily.infimum (upperTails f)8586noncomputable def lowerEnvelope (f : BoundedFamily ι) : ℝ :=87  BoundedFamily.supremum (lowerTails f)8889theorem upperEnvelope_nonexpansive [Nonempty ι] :90    LipschitzWith 1 (upperEnvelope : BoundedFamily ι → ℝ) := by91  change LipschitzWith 1 (fun f : BoundedFamily ι => BoundedFamily.infimum (upperTails f))92  simpa only [mul_one, Function.comp_def, upperEnvelope] using93    BoundedFamily.infimum_nonexpansive.comp upperTails_nonexpansive9495theorem lowerEnvelope_nonexpansive [Nonempty ι] :96    LipschitzWith 1 (lowerEnvelope : BoundedFamily ι → ℝ) := by97  change LipschitzWith 1 (fun f : BoundedFamily ι => BoundedFamily.supremum (lowerTails f))98  simpa only [mul_one, Function.comp_def, lowerEnvelope] using99    BoundedFamily.supremum_nonexpansive.comp lowerTails_nonexpansive100101end BFPP

SHA-256