ProfileExtension.lean

1import BFPP.OrdinalIndex2import BFPP.ProfileGeometry34/-! # Constant-tail extension of ordinal profiles -/56namespace BFPP.Profile78set_option autoImplicit false9open Set Order1011universe u12variable {ρ κ : Ordinal.{u}} [hρ : Fact (IsSuccLimit ρ)] [hκ : Fact (IsSuccLimit κ)]1314noncomputable def extendValue (a : Profile (OrdinalIndex ρ)) (i : OrdinalIndex κ) : ℝ := by15  classical16  exact if hi : i.val < ρ then a.val ⟨i.val, hi⟩ else a.tail1718theorem extendValue_bounds (a : Profile (OrdinalIndex ρ)) (i : OrdinalIndex κ) :19    0 ≤ a.extendValue i ∧ a.extendValue i ≤ 2 := by20  classical21  dsimp [extendValue]22  split_ifs with hi23  · exact ⟨a.nonneg _, a.le_two _⟩24  · exact ⟨a.tail_nonneg, a.tail_le_two⟩2526theorem extendValue_le_tail (a : Profile (OrdinalIndex ρ)) (i : OrdinalIndex κ) :27    a.extendValue i ≤ a.tail := by28  classical29  dsimp [extendValue]30  split_ifs with hi31  · exact a.le_tail _32  · exact le_rfl3334theorem extendValue_monotone (a : Profile (OrdinalIndex ρ)) :35    Monotone (a.extendValue : OrdinalIndex κ → ℝ) := by36  classical37  intro i j hij38  dsimp [extendValue]39  by_cases hi : i.val < ρ40  · by_cases hj : j.val < ρ41    · simp only [dif_pos hi, dif_pos hj]42      exact a.monotone hij43    · simp only [dif_pos hi, dif_neg hj]44      exact a.le_tail _45  · have hj : ¬ j.val < ρ := fun hj => hi (lt_of_le_of_lt hij hj)46    simp only [dif_neg hi, dif_neg hj]47    exact le_rfl4849noncomputable def extend (hρκ : ρ ≤ κ) (a : Profile (OrdinalIndex ρ)) :50    Profile (OrdinalIndex κ) := by51  let f : BoundedFamily (OrdinalIndex κ) := BoundedFamily.ofBound a.extendValue 252    (fun i => by rw [Real.norm_eq_abs, abs_of_nonneg (a.extendValue_bounds i).1]53                 exact (a.extendValue_bounds i).2)54  refine ⟨f, ?_, a.extendValue_monotone, fun i => a.extendValue_bounds i⟩55  classical56  change (if hi : (0 : Ordinal.{u}) < ρ then a.val ⟨0, hi⟩ else a.tail) = 057  rw [dif_pos hρ.out.pos]58  exact a.at_bot5960@[simp] theorem extend_apply (hρκ : ρ ≤ κ) (a : Profile (OrdinalIndex ρ)) (i : OrdinalIndex κ) :61    (a.extend hρκ).val i = a.extendValue i := rfl6263theorem extend_apply_lt (hρκ : ρ ≤ κ) (a : Profile (OrdinalIndex ρ)) (i : OrdinalIndex κ)64    (hi : i.val < ρ) : (a.extend hρκ).val i = a.val ⟨i.val, hi⟩ := by65  classical66  simp only [extend_apply, extendValue, dif_pos hi]6768theorem extend_apply_ge (hρκ : ρ ≤ κ) (a : Profile (OrdinalIndex ρ)) (i : OrdinalIndex κ)69    (hi : ρ ≤ i.val) : (a.extend hρκ).val i = a.tail := by70  classical71  simp only [extend_apply, extendValue, dif_neg (not_lt_of_ge hi)]7273theorem extend_at_source (hρκ : ρ ≤ κ) (a : Profile (OrdinalIndex ρ)) (i : OrdinalIndex ρ) :74    (a.extend hρκ).val ⟨i.val, lt_of_lt_of_le i.property hρκ⟩ = a.val i :=75  a.extend_apply_lt hρκ _ i.property7677@[simp] theorem tail_extend (hρκ : ρ ≤ κ) (a : Profile (OrdinalIndex ρ)) :78    (a.extend hρκ).tail = a.tail := by79  apply le_antisymm80  · exact ciSup_le a.extendValue_le_tail81  · apply ciSup_le82    intro i83    rw [← a.extend_at_source hρκ i]84    exact (a.extend hρκ).le_tail _8586theorem extend_nonexpansive (hρκ : ρ ≤ κ) :87    LipschitzWith 1 (extend hρκ : Profile (OrdinalIndex ρ) → Profile (OrdinalIndex κ)) := by88  classical89  apply LipschitzWith.of_dist_le_mul90  intro a b91  simp only [NNReal.coe_one, one_mul]92  change dist (a.extend hρκ).val (b.extend hρκ).val ≤ dist a b93  apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).mpr94  intro i95  by_cases hi : i.val < ρ96  · rw [a.extend_apply_lt hρκ i hi, b.extend_apply_lt hρκ i hi]97    exact BoundedFamily.abs_sub_apply_le_dist a.val b.val _98  · rw [a.extend_apply_ge hρκ i (le_of_not_gt hi), b.extend_apply_ge hρκ i (le_of_not_gt hi)]99    simpa only [NNReal.coe_one, one_mul, Real.dist_eq] using tail_nonexpansive.dist_le_mul a b100101theorem extend_isometry (hρκ : ρ ≤ κ) :102    Isometry (extend hρκ : Profile (OrdinalIndex ρ) → Profile (OrdinalIndex κ)) := by103  apply isometry_iff_dist_eq.mpr104  intro a b105  apply le_antisymm106  · simpa only [NNReal.coe_one, one_mul] using (extend_nonexpansive hρκ).dist_le_mul a b107  · change dist a.val b.val ≤ dist (a.extend hρκ) (b.extend hρκ)108    apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).mpr109    intro i110    rw [← a.extend_at_source hρκ i, ← b.extend_at_source hρκ i]111    exact BoundedFamily.abs_sub_apply_le_dist (a.extend hρκ).val (b.extend hρκ).val _112113theorem extend_mix (hρκ : ρ ≤ κ) (a b : Profile (OrdinalIndex ρ)) (r s : ℝ)114    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) :115    (a.mix b r s hr hs hrs).extend hρκ =116      (a.extend hρκ).mix (b.extend hρκ) r s hr hs hrs := by117  classical118  letI : TopologicalSpace (OrdinalIndex κ) := ⊥119  apply Subtype.ext120  apply BoundedContinuousFunction.ext121  intro i122  by_cases hi : i.val < ρ123  · simp only [extend_apply_lt hρκ _ i hi, mix_apply]124  · have hge := le_of_not_gt hi125    simp only [extend_apply_ge hρκ _ i hge, mix_apply, tail_mix]126127end BFPP.Profile

SHA-256