EncodedRecurrence.lean

1import BFPP.EncodedMaps2import BFPP.TransfinitePropagator3import BFPP.DelayPrefixBound45/-! # The encoded delay is a transfinite contractive propagator -/67namespace BFPP89set_option autoImplicit false10open Set Order1112universe u13variable {ρ σ κ : Ordinal.{u}} [Fact (IsSuccLimit ρ)] [Fact (IsSuccLimit σ)]14    [hκ : Fact (IsSuccLimit κ)]1516theorem encodeProfiles_delay_interleave (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)17    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) :18    encodeProfiles hρκ hσκ z.delay =19      interleave (z.val.1.extend hρκ).delay.val (z.val.2.extend hσκ).delay.val := by20  change interleave (z.val.1.delay.extend hρκ).val (z.val.2.delay.extend hσκ).val = _21  rw [← Profile.extend_delay, ← Profile.extend_delay]2223theorem encodeProfiles_delay_causal (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)24    (z w : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (i : OrdinalIndex κ) :25    dist (encodeProfiles hρκ hσκ z.delay i) (encodeProfiles hρκ hσκ w.delay i) ≤26      dist (restrictFamily i.property.le (encodeProfiles hρκ hσκ z))27        (restrictFamily i.property.le (encodeProfiles hρκ hσκ w)) := by28  classical29  let c := dist (restrictFamily i.property.le (encodeProfiles hρκ hσκ z))30    (restrictFamily i.property.le (encodeProfiles hρκ hσκ w))31  change |encodeProfiles hρκ hσκ z.delay i - encodeProfiles hρκ hσκ w.delay i| ≤ c32  rw [encodeProfiles_delay_interleave, encodeProfiles_delay_interleave]33  rcases index_eq_even_or_odd κ i with he | ho34  · have hi : i.val % 2 = 0 := by rw [he]; exact evenIndex_mod _ _35    simp only [interleave, BoundedFamily.ofBound_apply, interleaveValue, if_pos hi,36      Profile.delay_apply]37    apply Profile.delayValue_abs_sub_le_of_prefix _ _ _ c dist_nonneg38    intro j hj39    have hj' : evenIndex κ j < i := by rw [he]; exact evenIndex_strictMono κ hj40    have hh := BoundedFamily.abs_sub_apply_le_dist41      (restrictFamily i.property.le (encodeProfiles hρκ hσκ z))42      (restrictFamily i.property.le (encodeProfiles hρκ hσκ w))43      ⟨(evenIndex κ j).val, hj'⟩44    change |encodeProfiles hρκ hσκ z (evenIndex κ j) -45      encodeProfiles hρκ hσκ w (evenIndex κ j)| ≤ c at hh46    rw [encodeProfiles_even, encodeProfiles_even] at hh47    exact hh48  · have hi₁ : i.val % 2 = 1 := by rw [ho]; exact oddIndex_mod _ _49    have hi : i.val % 2 ≠ 0 := by rw [hi₁]; norm_num50    simp only [interleave, BoundedFamily.ofBound_apply, interleaveValue, if_neg hi,51      add_sub_add_left_eq_sub, Profile.delay_apply]52    apply Profile.delayValue_abs_sub_le_of_prefix _ _ _ c dist_nonneg53    intro j hj54    have hj' : oddIndex κ j < i := by rw [ho]; exact oddIndex_strictMono κ hj55    have hh := BoundedFamily.abs_sub_apply_le_dist56      (restrictFamily i.property.le (encodeProfiles hρκ hσκ z))57      (restrictFamily i.property.le (encodeProfiles hρκ hσκ w))58      ⟨(oddIndex κ j).val, hj'⟩59    change |encodeProfiles hρκ hσκ z (oddIndex κ j) -60      encodeProfiles hρκ hσκ w (oddIndex κ j)| ≤ c at hh61    rw [encodeProfiles_odd, encodeProfiles_odd, add_sub_add_left_eq_sub] at hh62    exact hh6364theorem encodeProfiles_delay_limit (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)65    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (i : OrdinalIndex κ)66    (hi : IsSuccLimit i.val) :67    encodeProfiles hρκ hσκ z.delay i =68      lowerEnvelope (restrictFamily i.property.le (encodeProfiles hρκ hσκ z)) := by69  letI : Fact (IsSuccLimit i.val) := ⟨hi⟩70  have he : evenIndex κ i = i := Subtype.ext (ordinal_two_mul_limit i.val hi)71  have hprefix := interleave_lowerEnvelope_prefix i.property72    (z.val.1.extend hρκ) (z.val.2.extend hσκ)73  calc74    encodeProfiles hρκ hσκ z.delay i =75        encodeProfiles hρκ hσκ z.delay (evenIndex κ i) :=76      congrArg (encodeProfiles hρκ hσκ z.delay) he.symm77    _ = (z.val.1.delay.extend hρκ).val i := encodeProfiles_even hρκ hσκ z.delay i78    _ = (z.val.1.extend hρκ).delay.val i := by rw [← Profile.extend_delay]79    _ = lowerEnvelope (restrictFamily i.property.le (encodeProfiles hρκ hσκ z)) := hprefix.symm8081theorem encodedPropagator_isTCP (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) :82    IsTCP (encodedSet hρκ hσκ) (encodedPropagator hρκ hσκ) := by83  apply isTCP_of_causal (encodedPropagator hρκ hσκ) hκ.out.pos84    (encodedSet_nonempty hρκ hσκ) 085  · intro x86    obtain ⟨z, rfl⟩ := (encodeIso hρκ hσκ).surjective x87    rw [encodedPropagator_encode]88    change encodeProfiles hρκ hσκ z.delay ⊥ = 089    have h := encodeProfiles_even hρκ hσκ z.delay ⊥90    simpa only [evenIndex_bot, Profile.at_bot] using h91  · intro i x y92    obtain ⟨z, rfl⟩ := (encodeIso hρκ hσκ).surjective x93    obtain ⟨w, rfl⟩ := (encodeIso hρκ hσκ).surjective y94    rw [encodedPropagator_encode, encodedPropagator_encode]95    exact encodeProfiles_delay_causal hρκ hσκ z w i96  · intro i hi x97    obtain ⟨z, rfl⟩ := (encodeIso hρκ hσκ).surjective x98    rw [encodedPropagator_encode]99    exact encodeProfiles_delay_limit hρκ hσκ z i hi100101end BFPP

SHA-256