Regularization.lean

1import BFPP.Profiles2import Mathlib.Topology.Order.SuccPred34/-! # Successor--limit formulas and continuous regularization -/56namespace BFPP78set_option autoImplicit false910open Set Order Filter Topology1112universe u13variable {ι : Type u} [LinearOrder ι] [OrderBot ι]1415namespace Profile1617theorem delayValue_succ [SuccOrder ι] [NoMaxOrder ι] (a : Profile ι) (i : ι) :18    a.delayValue (Order.succ i) = a.val i := by19  classical20  have hne : Order.succ i ≠ ⊥ := ne_of_gt (lt_of_le_of_lt bot_le (Order.lt_succ i))21  rw [delayValue, if_neg hne]22  letI : Nonempty (Iio (Order.succ i)) := ⟨⟨i, Order.lt_succ i⟩⟩23  apply le_antisymm24  · exact ciSup_le (fun j => a.monotone (Order.lt_succ_iff.mp j.property))25  · exact le_ciSup (a.prefix_bddAbove _) ⟨i, Order.lt_succ i⟩2627noncomputable def regularizeValue (a : Profile ι) (i : ι) : ℝ := by28  classical29  exact if IsSuccLimit i then a.delayValue i else a.val i3031theorem regularizeValue_nonneg (a : Profile ι) (i : ι) : 0 ≤ a.regularizeValue i := by32  classical33  unfold regularizeValue34  split_ifs35  · exact a.delayValue_nonneg i36  · exact a.nonneg i3738theorem regularizeValue_le_apply (a : Profile ι) (i : ι) : a.regularizeValue i ≤ a.val i := by39  classical40  unfold regularizeValue41  split_ifs42  · exact a.delayValue_le_apply i43  · exact le_rfl4445theorem delayValue_le_regularizeValue (a : Profile ι) (i : ι) :46    a.delayValue i ≤ a.regularizeValue i := by47  classical48  unfold regularizeValue49  split_ifs50  · exact le_rfl51  · exact a.delayValue_le_apply i5253@[simp] theorem regularizeValue_bot (a : Profile ι) : a.regularizeValue ⊥ = 0 := by54  simp [regularizeValue, not_isSuccLimit_bot, a.at_bot]5556@[simp] theorem regularizeValue_succ [SuccOrder ι] [NoMaxOrder ι] (a : Profile ι) (i : ι) :57    a.regularizeValue (Order.succ i) = a.val (Order.succ i) := by58  simp [regularizeValue, not_isSuccLimit_succ]5960theorem regularizeValue_limit (a : Profile ι) (i : ι) (hi : IsSuccLimit i) :61    a.regularizeValue i = ⨆ j : Iio i, a.val j.val := by62  simp [regularizeValue, hi, delayValue, hi.ne_bot]6364theorem regularizeValue_monotone (a : Profile ι) : Monotone a.regularizeValue := by65  classical66  intro i j hij67  rcases hij.eq_or_lt with rfl | hij68  · exact le_rfl69  by_cases hj : IsSuccLimit j70  · rw [regularizeValue_limit a j hj]71    exact (a.regularizeValue_le_apply i).trans (le_ciSup (a.prefix_bddAbove j) ⟨i, hij⟩)72  · have he : a.regularizeValue j = a.val j := by simp [regularizeValue, hj]73    rw [he]74    exact (a.regularizeValue_le_apply i).trans (a.monotone hij.le)7576noncomputable def regularize (a : Profile ι) : Profile ι := by77  let f : BoundedFamily ι := BoundedFamily.ofBound a.regularizeValue 2 (fun i => by78    rw [Real.norm_eq_abs, abs_of_nonneg (a.regularizeValue_nonneg i)]79    exact (a.regularizeValue_le_apply i).trans (a.le_two i))80  exact ⟨f, a.regularizeValue_bot, a.regularizeValue_monotone,81    fun i => ⟨a.regularizeValue_nonneg i,82      (a.regularizeValue_le_apply i).trans (a.le_two i)⟩⟩8384@[simp] theorem regularize_apply (a : Profile ι) (i : ι) :85    a.regularize.val i = a.regularizeValue i := rfl8687theorem regularize_le (a : Profile ι) : a.regularize ≤ a := a.regularizeValue_le_apply8889theorem regularize_nonexpansive : LipschitzWith 1 (regularize : Profile ι → Profile ι) := by90  apply LipschitzWith.of_dist_le_mul91  intro a b92  simp only [NNReal.coe_one, one_mul]93  change dist a.regularize.val b.regularize.val ≤ dist a b94  apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).295  intro i96  classical97  by_cases hi : IsSuccLimit i98  · simp only [regularize_apply, regularizeValue, if_pos hi]99    have h := delay_nonexpansive.dist_le_mul a b100    have hd : |a.delayValue i - b.delayValue i| ≤ dist a.delay b.delay :=101      BoundedFamily.abs_sub_apply_le_dist a.delay.val b.delay.val i102    exact hd.trans (by simpa only [NNReal.coe_one, one_mul] using h)103  · simp only [regularize_apply, regularizeValue, if_neg hi]104    exact BoundedFamily.abs_sub_apply_le_dist a.val b.val i105106theorem tail_regularize [NoMaxOrder ι] (a : Profile ι) : a.regularize.tail = a.tail := by107  apply le_antisymm108  · exact ciSup_le (fun i => (a.regularizeValue_le_apply i).trans (a.le_tail i))109  · rw [← a.tail_delay]110    exact ciSup_le (fun i => (a.delayValue_le_regularizeValue i).trans (a.regularize.le_tail i))111112/-- Regularization is continuous for the actual order topology, not the discrete113topology used to present the ambient space of bounded families. -/114theorem regularizeValue_continuous [SuccOrder ι] [NoMaxOrder ι]115    [TopologicalSpace ι] [OrderTopology ι] (a : Profile ι) : Continuous a.regularizeValue := by116  apply continuous_iff_continuousAt.mpr117  intro i118  by_cases hi : IsSuccLimit i119  · apply Metric.continuousAt_iff'.mpr120    intro ε hε121    letI : Nonempty (Iio i) := hi.nonempty_Iio.to_subtype122    have happrox : a.regularizeValue i - ε < ⨆ j : Iio i, a.val j.val := by123      rw [← regularizeValue_limit a i hi]124      linarith125    obtain ⟨j, hj⟩ := exists_lt_of_lt_ciSup happrox126    have hs : Order.succ j.val < i := hi.succ_lt j.property127    have hn : Ioo (Order.succ j.val) (Order.succ i) ∈ 𝓝 i :=128      isOpen_Ioo.mem_nhds ⟨hs, Order.lt_succ i⟩129    filter_upwards [hn] with k hk130    have hki : k ≤ i := Order.lt_succ_iff.mp hk.2131    have hupper := a.regularizeValue_monotone hki132    have hlower : a.val j.val ≤ a.regularizeValue k := by133      calc134        a.val j.val ≤ a.val (Order.succ j.val) := a.monotone (Order.le_succ _)135        _ = a.regularizeValue (Order.succ j.val) := (regularizeValue_succ _ _).symm136        _ ≤ a.regularizeValue k := a.regularizeValue_monotone hk.1.le137    rw [Real.dist_eq, abs_of_nonpos (sub_nonpos.mpr hupper)]138    linarith139  · rw [ContinuousAt, SuccOrder.nhds_eq_pure.mpr hi]140    exact tendsto_pure_nhds _ _141142end Profile143end BFPP

SHA-256