Interleaving.lean

1import BFPP.OrdinalPairs23/-! # Affine isometric interleaving of two bounded channels -/45namespace BFPP67set_option autoImplicit false8open Set Order910universe u11variable {κ : Ordinal.{u}} [Fact (IsSuccLimit κ)]1213noncomputable def interleaveValue (a b : BoundedFamily (OrdinalIndex κ)) (i : OrdinalIndex κ) : ℝ := by14  classical15  exact if i.val % 2 = 0 then a (halfIndex κ i) else 4 + b (halfIndex κ i)1617noncomputable def interleave (a b : BoundedFamily (OrdinalIndex κ)) : BoundedFamily (OrdinalIndex κ) :=18  BoundedFamily.ofBound (interleaveValue a b) (‖a‖ + ‖b‖ + 4) (by19    intro i20    classical21    rw [Real.norm_eq_abs]22    dsimp [interleaveValue]23    split_ifs24    · have ha := a.abs_apply_le_norm (halfIndex κ i)25      linarith [norm_nonneg b]26    · calc27        |4 + b (halfIndex κ i)| ≤ |(4 : ℝ)| + |b (halfIndex κ i)| := abs_add_le _ _28        _ ≤ ‖a‖ + ‖b‖ + 4 := by29          have hb := b.abs_apply_le_norm (halfIndex κ i)30          norm_num31          linarith [norm_nonneg a])3233@[simp] theorem interleave_even (a b : BoundedFamily (OrdinalIndex κ)) (i : OrdinalIndex κ) :34    interleave a b (evenIndex κ i) = a i := by35  classical36  simp [interleave, interleaveValue]3738@[simp] theorem interleave_odd (a b : BoundedFamily (OrdinalIndex κ)) (i : OrdinalIndex κ) :39    interleave a b (oddIndex κ i) = 4 + b i := by40  classical41  simp [interleave, interleaveValue]4243theorem interleave_isometry :44    Isometry (fun p : BoundedFamily (OrdinalIndex κ) × BoundedFamily (OrdinalIndex κ) =>45      interleave p.1 p.2) := by46  classical47  apply isometry_iff_dist_eq.mpr48  intro p q49  apply le_antisymm50  · apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).mpr51    intro i52    rcases index_eq_even_or_odd κ i with he | ho53    · rw [he, interleave_even, interleave_even]54      exact (p.1.abs_sub_apply_le_dist q.1 _).trans (le_max_left _ _)55    · rw [ho, interleave_odd, interleave_odd, add_sub_add_left_eq_sub]56      exact (p.2.abs_sub_apply_le_dist q.2 _).trans (le_max_right _ _)57  · apply max_le58    · apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).mpr59      intro i60      rw [← interleave_even p.1 p.2 i, ← interleave_even q.1 q.2 i]61      exact BoundedFamily.abs_sub_apply_le_dist _ _ _62    · apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).mpr63      intro i64      have h := BoundedFamily.abs_sub_apply_le_dist (interleave p.1 p.2) (interleave q.1 q.2)65        (oddIndex κ i)66      simpa only [interleave_odd, add_sub_add_left_eq_sub] using h6768theorem interleave_affine (a b a' b' : BoundedFamily (OrdinalIndex κ))69    (r s : ℝ) (hrs : r + s = 1) :70    interleave (r • a + s • a') (r • b + s • b') =71      r • interleave a b + s • interleave a' b' := by72  classical73  letI : TopologicalSpace (OrdinalIndex κ) := ⊥74  apply BoundedContinuousFunction.ext75  intro i76  rcases index_eq_even_or_odd κ i with he | ho77  · rw [he]78    simp only [BoundedContinuousFunction.add_apply, BoundedContinuousFunction.smul_apply,79      interleave_even]80  · rw [ho]81    simp only [BoundedContinuousFunction.add_apply, BoundedContinuousFunction.smul_apply,82      interleave_odd]83    change 4 + (r * b _ + s * b' _) = r * (4 + b _) + s * (4 + b' _)84    nlinarith [hrs]8586end BFPP

SHA-256