Profiles.lean

1import BFPP.BoundedFamilies2import Mathlib.Order.WellFounded3import Mathlib.Analysis.Convex.Basic45/-!6# Increasing profiles and transfinite delay78The index is any linear order with a least element. `delayValue` is uniformly9the supremum over strict predecessors, except at the least element. On ordinal10indices this is the successor--limit formula of the paper.11-/1213namespace BFPP1415set_option autoImplicit false1617open Set1819universe u20variable {ι : Type u} [LinearOrder ι] [OrderBot ι]2122def profileSet (ι : Type u) [LinearOrder ι] [OrderBot ι] : Set (BoundedFamily ι) :=23  {a | a ⊥ = 0 ∧ Monotone a ∧ ∀ i, a i ∈ Icc (0 : ℝ) 2}2425abbrev Profile (ι : Type u) [LinearOrder ι] [OrderBot ι] :=26  {a : BoundedFamily ι // a ∈ profileSet ι}2728namespace Profile2930theorem at_bot (a : Profile ι) : a.val ⊥ = 0 := a.property.131theorem monotone (a : Profile ι) : Monotone a.val := a.property.2.132theorem nonneg (a : Profile ι) (i : ι) : 0 ≤ a.val i := (a.property.2.2 i).133theorem le_two (a : Profile ι) (i : ι) : a.val i ≤ 2 := (a.property.2.2 i).23435noncomputable def tail (a : Profile ι) : ℝ := BoundedFamily.supremum a.val3637theorem le_tail (a : Profile ι) (i : ι) : a.val i ≤ a.tail :=38  le_ciSup a.val.bddAbove_range i3940theorem tail_nonneg (a : Profile ι) : 0 ≤ a.tail :=41  (a.nonneg ⊥).trans (a.le_tail ⊥)4243theorem tail_le_two (a : Profile ι) : a.tail ≤ 2 := ciSup_le a.le_two4445theorem tail_nonexpansive : LipschitzWith 1 (tail : Profile ι → ℝ) := by46  apply LipschitzWith.of_dist_le_mul47  intro a b48  exact BoundedFamily.supremum_nonexpansive.dist_le_mul a.val b.val4950noncomputable def delayValue (a : Profile ι) (i : ι) : ℝ := by51  classical52  exact if i = ⊥ then 0 else ⨆ j : Iio i, a.val j.val5354@[simp] theorem delayValue_bot (a : Profile ι) : a.delayValue ⊥ = 0 := by55  simp [delayValue]5657theorem prefix_bddAbove (a : Profile ι) (i : ι) :58    BddAbove (range (fun j : Iio i => a.val j.val)) := by59  refine ⟨2, ?_⟩60  rintro _ ⟨j, rfl⟩61  exact a.le_two j.val6263theorem delayValue_nonneg (a : Profile ι) (i : ι) : 0 ≤ a.delayValue i := by64  classical65  by_cases hi : i = ⊥66  · simp [delayValue, hi]67  · rw [delayValue, if_neg hi]68    have hbot : (⊥ : ι) < i := lt_of_le_of_ne bot_le (Ne.symm hi)69    exact (a.nonneg ⊥).trans (le_ciSup (a.prefix_bddAbove i) ⟨⊥, hbot⟩)7071theorem delayValue_le_apply (a : Profile ι) (i : ι) : a.delayValue i ≤ a.val i := by72  classical73  by_cases hi : i = ⊥74  · simp [hi, a.at_bot]75  · rw [delayValue, if_neg hi]76    have hbot : (⊥ : ι) < i := lt_of_le_of_ne bot_le (Ne.symm hi)77    letI : Nonempty (Iio i) := ⟨⟨⊥, hbot⟩⟩78    exact ciSup_le (fun j => a.monotone j.property.le)7980theorem delayValue_le_two (a : Profile ι) (i : ι) : a.delayValue i ≤ 2 :=81  (a.delayValue_le_apply i).trans (a.le_two i)8283theorem delayValue_monotone (a : Profile ι) : Monotone a.delayValue := by84  classical85  intro i j hij86  by_cases hi : i = ⊥87  · simpa [hi] using a.delayValue_nonneg j88  have hj : j ≠ ⊥ := by89    intro h90    exact hi (bot_unique (h ▸ hij))91  have hbot : (⊥ : ι) < i := lt_of_le_of_ne bot_le (Ne.symm hi)92  letI : Nonempty (Iio i) := ⟨⟨⊥, hbot⟩⟩93  rw [delayValue, if_neg hi, delayValue, if_neg hj]94  apply ciSup_le95  intro k96  exact le_ciSup (a.prefix_bddAbove j) ⟨k.val, lt_of_lt_of_le k.property hij⟩9798noncomputable def delay (a : Profile ι) : Profile ι := by99  let f : BoundedFamily ι := BoundedFamily.ofBound a.delayValue 2 (fun i => by100    rw [Real.norm_eq_abs, abs_of_nonneg (a.delayValue_nonneg i)]101    exact a.delayValue_le_two i)102  exact ⟨f, a.delayValue_bot, a.delayValue_monotone,103    fun i => ⟨a.delayValue_nonneg i, a.delayValue_le_two i⟩⟩104105@[simp] theorem delay_apply (a : Profile ι) (i : ι) : a.delay.val i = a.delayValue i := rfl106107theorem delay_le (a : Profile ι) : a.delay ≤ a := a.delayValue_le_apply108109theorem delay_nonexpansive : LipschitzWith 1 (delay : Profile ι → Profile ι) := by110  apply LipschitzWith.of_dist_le_mul111  intro a b112  simp only [NNReal.coe_one, one_mul]113  change dist a.delay.val b.delay.val ≤ dist a b114  apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).2115  intro i116  classical117  by_cases hi : i = ⊥118  · simpa [hi] using (dist_nonneg : 0 ≤ dist a b)119  · have hbot : (⊥ : ι) < i := lt_of_le_of_ne bot_le (Ne.symm hi)120    letI : Nonempty (Iio i) := ⟨⟨⊥, hbot⟩⟩121    simp only [delay_apply, delayValue, if_neg hi]122    apply abs_ciSup_sub_ciSup_le _ _ (a.prefix_bddAbove i) (b.prefix_bddAbove i)123    intro j124    exact BoundedFamily.abs_sub_apply_le_dist a.val b.val j.val125126theorem subsolution_eq_zero [WellFoundedLT ι] (a : Profile ι) (h : a ≤ a.delay) :127    ∀ i, a.val i = 0 := by128  intro i129  induction i using WellFoundedLT.induction with130  | ind i ih =>131    classical132    by_cases hi : i = ⊥133    · simpa [hi] using a.at_bot134    have hbot : (⊥ : ι) < i := lt_of_le_of_ne bot_le (Ne.symm hi)135    letI : Nonempty (Iio i) := ⟨⟨⊥, hbot⟩⟩136    have hz : a.delayValue i = 0 := by137      simp only [delayValue, if_neg hi]138      have hfun : (fun j : Iio i => a.val j.val) = (fun _ : Iio i => (0 : ℝ)) :=139        funext (fun j => ih j.val j.property)140      rw [hfun, ciSup_const]141    have hle : a.val i ≤ a.delayValue i := h i142    exact le_antisymm (hz ▸ hle) (a.nonneg i)143144theorem tail_delay [NoMaxOrder ι] (a : Profile ι) : a.delay.tail = a.tail := by145  classical146  apply le_antisymm147  · apply ciSup_le148    intro i149    exact (a.delayValue_le_apply i).trans (a.le_tail i)150  · apply ciSup_le151    intro i152    obtain ⟨j, hij⟩ := exists_gt i153    have hj : j ≠ ⊥ := ne_of_gt (lt_of_le_of_lt bot_le hij)154    calc155      a.val i ≤ a.delay.val j := by156        simp only [delay_apply, delayValue, if_neg hj]157        exact le_ciSup (a.prefix_bddAbove j) ⟨i, hij⟩158      _ ≤ a.delay.tail := a.delay.le_tail j159160end Profile161end BFPP

SHA-256