EncodedDomain.lean

1import BFPP.Interleaving2import BFPP.ExtensionDelay3import BFPP.TwoProfileStructure45/-! # A closed bounded convex domain in a single ordinal sequence space -/67namespace BFPP89set_option autoImplicit false10open Set Order1112universe u13variable {ρ σ κ : Ordinal.{u}} [Fact (IsSuccLimit ρ)] [Fact (IsSuccLimit σ)] [Fact (IsSuccLimit κ)]1415noncomputable def encodeProfiles (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)16    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) : BoundedFamily (OrdinalIndex κ) :=17  interleave (z.val.1.extend hρκ).val (z.val.2.extend hσκ).val1819@[simp] theorem encodeProfiles_even (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)20    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (i : OrdinalIndex κ) :21    encodeProfiles hρκ hσκ z (evenIndex κ i) = (z.val.1.extend hρκ).val i :=22  interleave_even _ _ _2324@[simp] theorem encodeProfiles_odd (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)25    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (i : OrdinalIndex κ) :26    encodeProfiles hρκ hσκ z (oddIndex κ i) = 4 + (z.val.2.extend hσκ).val i :=27  interleave_odd _ _ _2829theorem encodeProfiles_isometry (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) :30    Isometry (encodeProfiles hρκ hσκ) := by31  apply isometry_iff_dist_eq.mpr32  intro z w33  rw [encodeProfiles, encodeProfiles, interleave_isometry.dist_eq34    ((z.val.1.extend hρκ).val, (z.val.2.extend hσκ).val)35    ((w.val.1.extend hρκ).val, (w.val.2.extend hσκ).val)]36  change max (dist (z.val.1.extend hρκ) (w.val.1.extend hρκ))37    (dist (z.val.2.extend hσκ) (w.val.2.extend hσκ)) =38      max (dist z.val.1 w.val.1) (dist z.val.2 w.val.2)39  rw [(Profile.extend_isometry hρκ).dist_eq, (Profile.extend_isometry hσκ).dist_eq]4041theorem encodeProfiles_mix (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)42    (z w : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (r s : ℝ)43    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) :44    encodeProfiles hρκ hσκ (z.mix w r s hr hs hrs) =45      r • encodeProfiles hρκ hσκ z + s • encodeProfiles hρκ hσκ w := by46  simp only [encodeProfiles, TwoProfile.mix_first, TwoProfile.mix_second, Profile.extend_mix]47  exact interleave_affine _ _ _ _ r s hrs4849def encodedSet (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) : Set (BoundedFamily (OrdinalIndex κ)) :=50  range (encodeProfiles hρκ hσκ)5152theorem encodedSet_nonempty (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) : (encodedSet hρκ hσκ).Nonempty :=53  ⟨encodeProfiles hρκ hσκ TwoProfile.witness, mem_range_self _⟩5455theorem encodedSet_isClosed (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) : IsClosed (encodedSet hρκ hσκ) :=56  (encodeProfiles_isometry hρκ hσκ).isUniformInducing.isComplete_range.isClosed5758theorem encodedSet_convex (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) : Convex ℝ (encodedSet hρκ hσκ) := by59  intro x hx y hy r s hr hs hrs60  obtain ⟨z, rfl⟩ := hx61  obtain ⟨w, rfl⟩ := hy62  exact ⟨z.mix w r s hr hs hrs, encodeProfiles_mix hρκ hσκ z w r s hr hs hrs⟩6364theorem encodeProfiles_norm_le (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)65    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) : ‖encodeProfiles hρκ hσκ z‖ ≤ 6 := by66  letI : TopologicalSpace (OrdinalIndex κ) := ⊥67  apply (BoundedContinuousFunction.norm_le (by norm_num : (0 : ℝ) ≤ 6)).mpr68  intro i69  rw [Real.norm_eq_abs]70  rcases index_eq_even_or_odd κ i with he | ho71  · rw [he, encodeProfiles_even, abs_of_nonneg ((z.val.1.extend hρκ).nonneg _)]72    exact ((z.val.1.extend hρκ).le_two _).trans (by norm_num)73  · rw [ho, encodeProfiles_odd]74    have hb₀ := (z.val.2.extend hσκ).nonneg (halfIndex κ i)75    have hb₁ := (z.val.2.extend hσκ).le_two (halfIndex κ i)76    exact abs_le.mpr ⟨by linarith, by linarith⟩7778theorem encodedSet_isBounded (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) :79    Bornology.IsBounded (encodedSet hρκ hσκ) := by80  apply (Metric.isBounded_closedBall (x := (0 : BoundedFamily (OrdinalIndex κ))) (r := 6)).subset81  rintro x ⟨z, rfl⟩82  simpa only [Metric.mem_closedBall, dist_zero_right] using encodeProfiles_norm_le hρκ hσκ z8384abbrev EncodedDomain (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) :=85  {x : BoundedFamily (OrdinalIndex κ) // x ∈ encodedSet hρκ hσκ}8687noncomputable def encodeIso (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) :88    TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ) ≃ᵢ EncodedDomain hρκ hσκ where89  toFun z := ⟨encodeProfiles hρκ hσκ z, mem_range_self z⟩90  invFun x := x.property.choose91  left_inv z := (encodeProfiles_isometry hρκ hσκ).injective (Exists.choose_spec (mem_range_self z))92  right_inv x := Subtype.ext x.property.choose_spec93  isometry_toFun := encodeProfiles_isometry hρκ hσκ9495end BFPP

SHA-256