InterleavingEnvelopes.lean

1import BFPP.Interleaving2import BFPP.EnvelopeOrder3import Mathlib.Order.Cofinal45/-! # Separated interleaved channels are recovered by the two envelopes -/67namespace BFPP89set_option autoImplicit false10open Set Order1112universe u13variable {κ : Ordinal.{u}} [Fact (IsSuccLimit κ)]1415theorem evenIndex_cofinal : IsCofinal (range (evenIndex κ)) :=16  isCofinal_range_of_strictMono (evenIndex_strictMono κ)1718theorem oddIndex_cofinal : IsCofinal (range (oddIndex κ)) :=19  isCofinal_range_of_strictMono (oddIndex_strictMono κ)2021theorem halfIndex_monotone : Monotone (halfIndex κ) := by22  intro i j hij23  exact (Ordinal.mul_div_gc (by norm_num : (2 : Ordinal.{u}) ≠ 0)).monotone_u hij2425theorem interleave_lowerEnvelope (a b : Profile (OrdinalIndex κ)) :26    lowerEnvelope (interleave a.val b.val) = a.tail := by27  apply le_antisymm28  · apply lowerEnvelope_le29    intro i30    obtain ⟨_, ⟨j, rfl⟩, hij⟩ := evenIndex_cofinal i31    calc32      lowerTail (interleave a.val b.val) i ≤ interleave a.val b.val (evenIndex κ j) :=33        lowerTail_le_point _ _ _ hij34      _ = a.val j := interleave_even _ _ _35      _ ≤ a.tail := a.le_tail j36  · apply ciSup_le37    intro j38    apply le_trans ?_ (lowerTail_le_lowerEnvelope (interleave a.val b.val) (evenIndex κ j))39    apply le_lowerTail40    intro i hji41    have hjhalf : j ≤ halfIndex κ i := by42      have h := halfIndex_monotone hji43      simpa only [half_evenIndex] using h44    rcases index_eq_even_or_odd κ i with he | ho45    · rw [he, interleave_even]46      exact a.monotone hjhalf47    · rw [ho, interleave_odd]48      have ha := a.le_two j49      have hb := b.nonneg (halfIndex κ i)50      linarith5152theorem interleave_upperEnvelope (a b : Profile (OrdinalIndex κ)) :53    upperEnvelope (interleave a.val b.val) = 4 + b.tail := by54  apply le_antisymm55  · apply le_trans (upperEnvelope_le_upperTail (interleave a.val b.val) ⊥)56    apply upperTail_le57    intro i _58    rcases index_eq_even_or_odd κ i with he | ho59    · rw [he, interleave_even]60      have ha := a.le_two (halfIndex κ i)61      have hb := b.tail_nonneg62      linarith63    · rw [ho, interleave_odd]64      exact add_le_add le_rfl (b.le_tail _)65  · apply le_upperEnvelope66    intro i67    have h : b.tail ≤ upperTail (interleave a.val b.val) i - 4 := by68      apply ciSup_le69      intro j70      obtain ⟨_, ⟨k, rfl⟩, hk⟩ := oddIndex_cofinal (max i (oddIndex κ j))71      have hik : i ≤ oddIndex κ k := (le_max_left _ _).trans hk72      have hjk : j ≤ k := (oddIndex_strictMono κ).le_iff_le.mp ((le_max_right _ _).trans hk)73      have hpoint := point_le_upperTail (interleave a.val b.val) i (oddIndex κ k) hik74      rw [interleave_odd] at hpoint75      have hmono := b.monotone hjk76      linarith77    linarith7879end BFPP

SHA-256