ProfileRestriction.lean

1import BFPP.ExtensionDelay2import BFPP.InterleavingEnvelopes34/-! # Restriction to ordinal prefixes and the encoded limit formulas -/56namespace BFPP78set_option autoImplicit false9open Set Order1011universe u12variable {tau κ : Ordinal.{u}}1314noncomputable def restrictFamily (h : tau ≤ κ) (f : BoundedFamily (OrdinalIndex κ)) :15    BoundedFamily (OrdinalIndex tau) :=16  BoundedFamily.reindex (fun i => ⟨i.val, lt_of_lt_of_le i.property h⟩) f1718@[simp] theorem restrictFamily_apply (h : tau ≤ κ) (f : BoundedFamily (OrdinalIndex κ))19    (i : OrdinalIndex tau) :20    restrictFamily h f i = f ⟨i.val, lt_of_lt_of_le i.property h⟩ := rfl2122theorem restrictFamily_nonexpansive (h : tau ≤ κ) : LipschitzWith 1 (restrictFamily h) :=23  BoundedFamily.reindex_nonexpansive _2425variable [Fact (IsSuccLimit tau)] [Fact (IsSuccLimit κ)]2627noncomputable def Profile.restrict (h : tau ≤ κ) (a : Profile (OrdinalIndex κ)) :28    Profile (OrdinalIndex tau) := by29  refine ⟨restrictFamily h a.val, ?_, ?_, ?_⟩30  · exact a.at_bot31  · intro i j hij32    exact a.monotone hij33  · intro i34    exact ⟨a.nonneg _, a.le_two _⟩3536@[simp] theorem Profile.restrict_apply (h : tau ≤ κ) (a : Profile (OrdinalIndex κ))37    (i : OrdinalIndex tau) :38    (a.restrict h).val i = a.val ⟨i.val, lt_of_lt_of_le i.property h⟩ := rfl3940theorem Profile.tail_restrict (h : tau < κ) (a : Profile (OrdinalIndex κ)) :41    (a.restrict h.le).tail = a.delayValue ⟨tau, h⟩ := by42  apply le_antisymm43  · apply ciSup_le44    intro i45    exact a.le_delayValue_of_lt ⟨i.val, lt_trans i.property h⟩ ⟨tau, h⟩ i.property46  · apply a.delayValue_le_of_forall_lt ⟨tau, h⟩ _ (a.restrict h.le).tail_nonneg47    intro j hj48    exact (a.restrict h.le).le_tail ⟨j.val, hj⟩4950theorem restrictFamily_interleave (h : tau ≤ κ) (a b : Profile (OrdinalIndex κ)) :51    restrictFamily h (interleave a.val b.val) = interleave (a.restrict h).val (b.restrict h).val := by52  letI : TopologicalSpace (OrdinalIndex tau) := ⊥53  apply BoundedContinuousFunction.ext54  intro i55  rfl5657theorem interleave_lowerEnvelope_prefix (h : tau < κ) (a b : Profile (OrdinalIndex κ)) :58    lowerEnvelope (restrictFamily h.le (interleave a.val b.val)) = a.delayValue ⟨tau, h⟩ := by59  rw [restrictFamily_interleave, interleave_lowerEnvelope, Profile.tail_restrict]6061theorem interleave_upperEnvelope_prefix (h : tau < κ) (a b : Profile (OrdinalIndex κ)) :62    upperEnvelope (restrictFamily h.le (interleave a.val b.val)) = 4 + b.delayValue ⟨tau, h⟩ := by63  rw [restrictFamily_interleave, interleave_upperEnvelope, Profile.tail_restrict]6465end BFPP

SHA-256