Deficits.lean

1import BFPP.ContinuousBall2import BFPP.Profiles34/-! # Deficits over level sets, with the empty-set convention -/56namespace BFPP78set_option autoImplicit false910open Set1112universe u v13variable {K : Type u} [TopologicalSpace K] [CompactSpace K]1415noncomputable def deficit (s : Set K) (f : UnitBall C(K, ℝ)) : ℝ := by16  classical17  exact if s.Nonempty then ⨆ t : s, 1 - f.val t.val else 01819theorem deficit_range_bddAbove (s : Set K) (f : UnitBall C(K, ℝ)) :20    BddAbove (range (fun t : s => 1 - f.val t.val)) := by21  refine ⟨2, ?_⟩22  rintro _ ⟨t, rfl⟩23  have h := (continuousBall_bounds f t.val).124  linarith2526theorem deficit_nonneg (s : Set K) (f : UnitBall C(K, ℝ)) : 0 ≤ deficit s f := by27  classical28  by_cases hs : s.Nonempty29  · obtain ⟨t, ht⟩ := hs30    rw [deficit, if_pos ⟨t, ht⟩]31    have h : 0 ≤ 1 - f.val t := sub_nonneg.mpr (continuousBall_bounds f t).232    exact h.trans (le_ciSup (deficit_range_bddAbove s f) ⟨t, ht⟩)33  · simp [deficit, hs]3435theorem deficit_le_two (s : Set K) (f : UnitBall C(K, ℝ)) : deficit s f ≤ 2 := by36  classical37  by_cases hs : s.Nonempty38  · letI : Nonempty s := hs.to_subtype39    rw [deficit, if_pos hs]40    apply ciSup_le41    intro t42    have h := (continuousBall_bounds f t.val).143    linarith44  · simp [deficit, hs]4546@[simp] theorem deficit_empty (f : UnitBall C(K, ℝ)) : deficit ∅ f = 0 := by47  simp [deficit]4849theorem le_deficit (s : Set K) (f : UnitBall C(K, ℝ)) (t : K) (ht : t ∈ s) :50    1 - f.val t ≤ deficit s f := by51  classical52  rw [deficit, if_pos ⟨t, ht⟩]53  exact le_ciSup (deficit_range_bddAbove s f) ⟨t, ht⟩5455theorem deficit_le_of_pointwise (s : Set K) (f : UnitBall C(K, ℝ))56    (a : ℝ) (ha : 0 ≤ a) (h : ∀ t ∈ s, 1 - f.val t ≤ a) : deficit s f ≤ a := by57  classical58  by_cases hs : s.Nonempty59  · letI : Nonempty s := hs.to_subtype60    rw [deficit, if_pos hs]61    exact ciSup_le (fun t => h t.val t.property)62  · simpa [deficit, hs] using ha6364theorem deficit_mono (s t : Set K) (hst : s ⊆ t) (f : UnitBall C(K, ℝ)) :65    deficit s f ≤ deficit t f :=66  deficit_le_of_pointwise s f _ (deficit_nonneg t f)67    (fun x hx => le_deficit t f x (hst hx))6869theorem deficit_nonexpansive (s : Set K) :70    LipschitzWith 1 (deficit s : UnitBall C(K, ℝ) → ℝ) := by71  apply LipschitzWith.of_dist_le_mul72  intro f g73  simp only [NNReal.coe_one, one_mul, Real.dist_eq]74  classical75  by_cases hs : s.Nonempty76  · letI : Nonempty s := hs.to_subtype77    simp only [deficit, if_pos hs]78    apply abs_ciSup_sub_ciSup_le _ _ (deficit_range_bddAbove s f) (deficit_range_bddAbove s g)79    intro t80    calc81      |1 - f.val t.val - (1 - g.val t.val)| = |g.val t.val - f.val t.val| := by82        congr 183        ring84      _ = |f.val t.val - g.val t.val| := abs_sub_comm _ _85      _ ≤ dist f g := continuousMap_abs_sub_le_dist f.val g.val t.val86  · simpa [deficit, hs] using (dist_nonneg : 0 ≤ dist f g)8788variable {ι : Type v} [LinearOrder ι] [OrderBot ι]8990noncomputable def analysisProfile (F : ι → Set K) (hF : Monotone F) (hF₀ : F ⊥ = ∅)91    (f : UnitBall C(K, ℝ)) : Profile ι := by92  let a : BoundedFamily ι := BoundedFamily.ofBound (fun i => deficit (F i) f) 293    (fun i => by94      rw [Real.norm_eq_abs, abs_of_nonneg (deficit_nonneg _ _)]95      exact deficit_le_two _ _)96  refine ⟨a, ?_, ?_, ?_⟩97  · change deficit (F ⊥) f = 098    rw [hF₀, deficit_empty]99  · intro i j hij100    exact deficit_mono (F i) (F j) (hF hij) f101  · intro i102    exact ⟨deficit_nonneg _ _, deficit_le_two _ _⟩103104@[simp] theorem analysisProfile_apply (F : ι → Set K) (hF : Monotone F)105    (hF₀ : F ⊥ = ∅) (f : UnitBall C(K, ℝ)) (i : ι) :106    (analysisProfile F hF hF₀ f).val i = deficit (F i) f := rfl107108theorem analysisProfile_nonexpansive (F : ι → Set K) (hF : Monotone F) (hF₀ : F ⊥ = ∅) :109    LipschitzWith 1 (analysisProfile F hF hF₀) := by110  apply LipschitzWith.of_dist_le_mul111  intro f g112  simp only [NNReal.coe_one, one_mul]113  change dist (analysisProfile F hF hF₀ f).val (analysisProfile F hF hF₀ g).val ≤ dist f g114  apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).2115  intro i116  have h := (deficit_nonexpansive (F i)).dist_le_mul f g117  simpa only [analysisProfile_apply, NNReal.coe_one, one_mul, Real.dist_eq] using h118119/-- Continuity extends the tail lower bound from the union to its closure. -/120theorem analysisProfile_tail_at_closure (F : ι → Set K) (hF : Monotone F)121    (hF₀ : F ⊥ = ∅) (f : UnitBall C(K, ℝ)) (p : K)122    (hp : p ∈ closure (⋃ i, F i)) : 1 - f.val p ≤ (analysisProfile F hF hF₀ f).tail := by123  let a := analysisProfile F hF hF₀ f124  have hc : IsClosed {t | 1 - f.val t ≤ a.tail} :=125    isClosed_le (continuous_const.sub f.val.continuous) continuous_const126  apply closure_minimal (t := {t | 1 - f.val t ≤ a.tail}) _ hc hp127  intro t ht128  obtain ⟨i, hi⟩ := mem_iUnion.mp ht129  exact (le_deficit (F i) f t hi).trans (a.le_tail i)130131end BFPP

SHA-256