ExtensionDelay.lean

1import BFPP.ProfileExtension23/-! # Delay commutes with constant-tail extension -/45namespace BFPP.Profile67set_option autoImplicit false8open Set Order910universe u v1112theorem le_delayValue_of_lt {ι : Type v} [LinearOrder ι] [OrderBot ι]13    (a : Profile ι) (j i : ι) (hji : j < i) : a.val j ≤ a.delayValue i := by14  classical15  have hi : i ≠ ⊥ := ne_of_gt (lt_of_le_of_lt bot_le hji)16  rw [delayValue, if_neg hi]17  exact le_ciSup (a.prefix_bddAbove i) ⟨j, hji⟩1819theorem delayValue_le_of_forall_lt {ι : Type v} [LinearOrder ι] [OrderBot ι]20    (a : Profile ι) (i : ι) (c : ℝ) (hc : 0 ≤ c)21    (h : ∀ j, j < i → a.val j ≤ c) : a.delayValue i ≤ c := by22  classical23  by_cases hi : i = ⊥24  · simpa only [hi, delayValue_bot] using hc25  · letI : Nonempty (Iio i) := ⟨⟨⊥, lt_of_le_of_ne bot_le (Ne.symm hi)⟩⟩26    rw [delayValue, if_neg hi]27    exact ciSup_le (fun j => h j.val j.property)2829variable {ρ κ : Ordinal.{u}} [Fact (IsSuccLimit ρ)] [Fact (IsSuccLimit κ)]3031theorem extend_delay (hρκ : ρ ≤ κ) (a : Profile (OrdinalIndex ρ)) :32    (a.extend hρκ).delay = a.delay.extend hρκ := by33  classical34  letI : TopologicalSpace (OrdinalIndex κ) := ⊥35  apply Subtype.ext36  apply BoundedContinuousFunction.ext37  intro i38  rw [delay_apply]39  by_cases hi : i.val < ρ40  · rw [a.delay.extend_apply_lt hρκ i hi, delay_apply]41    apply le_antisymm42    · apply (a.extend hρκ).delayValue_le_of_forall_lt i _ (a.delayValue_nonneg ⟨i.val, hi⟩)43      intro j hji44      have hjρ : j.val < ρ := lt_trans hji hi45      rw [a.extend_apply_lt hρκ j hjρ]46      exact a.le_delayValue_of_lt ⟨j.val, hjρ⟩ ⟨i.val, hi⟩ hji47    · apply a.delayValue_le_of_forall_lt ⟨i.val, hi⟩ _ ((a.extend hρκ).delayValue_nonneg i)48      intro j hji49      let j' : OrdinalIndex κ := ⟨j.val, lt_of_lt_of_le j.property hρκ⟩50      have h := (a.extend hρκ).le_delayValue_of_lt j' i hji51      rwa [a.extend_at_source hρκ j] at h52  · have hge : ρ ≤ i.val := le_of_not_gt hi53    rw [a.delay.extend_apply_ge hρκ i hge, tail_delay]54    apply le_antisymm55    · exact (a.extend hρκ).delayValue_le_of_forall_lt i _ a.tail_nonneg56        (fun j _ => a.extendValue_le_tail j)57    · apply ciSup_le58      intro j59      let j' : OrdinalIndex κ := ⟨j.val, lt_of_lt_of_le j.property hρκ⟩60      have hji : j' < i := show j.val < i.val from lt_of_lt_of_le j.property hge61      have h := (a.extend hρκ).le_delayValue_of_lt j' i hji62      rwa [a.extend_at_source hρκ j] at h6364end BFPP.Profile

SHA-256