TwoProfiles.lean

1import BFPP.Profiles2import BFPP.Center34/-! # The invariant two-tail domain and its common center -/56namespace BFPP78set_option autoImplicit false910universe u v11variable {ι : Type u} {κ : Type v}12  [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]1314abbrev TwoProfile (ι : Type u) (κ : Type v)15    [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ] :=16  {z : Profile ι × Profile κ // 2 ≤ z.1.tail + z.2.tail}1718namespace TwoProfile1920noncomputable def center (z : TwoProfile ι κ) : ℝ :=21  commonCenter z.val.1.tail z.val.2.tail2223theorem center_bounds (z : TwoProfile ι κ) :24    -1 ≤ z.center ∧ z.center ≤ 1 ∧25    1 - z.val.1.tail ≤ z.center ∧ z.center ≤ z.val.2.tail - 1 :=26  commonCenter_bounds ⟨z.val.1.tail_nonneg, z.val.1.tail_le_two⟩27    ⟨z.val.2.tail_nonneg, z.val.2.tail_le_two⟩ z.property2829theorem center_nonexpansive : LipschitzWith 1 (center : TwoProfile ι κ → ℝ) := by30  apply LipschitzWith.of_dist_le_mul31  intro z w32  simp only [NNReal.coe_one, one_mul, Real.dist_eq]33  change |commonCenter z.val.1.tail z.val.2.tail -34    commonCenter w.val.1.tail w.val.2.tail| ≤ dist z w35  apply commonCenter_nonexpansive_bound36  · have h := Profile.tail_nonexpansive.dist_le_mul z.val.1 w.val.137    have hp : dist z.val.1 w.val.1 ≤ dist z w := le_max_left _ _38    apply le_trans _ hp39    simpa only [NNReal.coe_one, one_mul, Real.dist_eq] using h40  · have h := Profile.tail_nonexpansive.dist_le_mul z.val.2 w.val.241    have hp : dist z.val.2 w.val.2 ≤ dist z w := le_max_right _ _42    apply le_trans _ hp43    simpa only [NNReal.coe_one, one_mul, Real.dist_eq] using h4445section Delay4647variable [NoMaxOrder ι] [NoMaxOrder κ]4849noncomputable def delay (z : TwoProfile ι κ) : TwoProfile ι κ :=50  ⟨(z.val.1.delay, z.val.2.delay), by51    simpa only [Profile.tail_delay] using z.property⟩5253theorem delay_nonexpansive : LipschitzWith 1 (delay : TwoProfile ι κ → TwoProfile ι κ) := by54  apply LipschitzWith.of_dist_le_mul55  intro z w56  simp only [NNReal.coe_one, one_mul]57  change max (dist z.val.1.delay w.val.1.delay) (dist z.val.2.delay w.val.2.delay) ≤58    max (dist z.val.1 w.val.1) (dist z.val.2 w.val.2)59  apply max_le_max60  · simpa only [NNReal.coe_one, one_mul] using61      Profile.delay_nonexpansive.dist_le_mul z.val.1 w.val.162  · simpa only [NNReal.coe_one, one_mul] using63      Profile.delay_nonexpansive.dist_le_mul z.val.2 w.val.26465theorem no_subsolution [WellFoundedLT ι] [WellFoundedLT κ] (z : TwoProfile ι κ) :66    ¬ z ≤ z.delay := by67  intro h68  have ha := Profile.subsolution_eq_zero z.val.1 h.169  have hb := Profile.subsolution_eq_zero z.val.2 h.270  have hA : z.val.1.tail = 0 := by71    simp only [Profile.tail, BoundedFamily.supremum, ha, ciSup_const]72  have hB : z.val.2.tail = 0 := by73    simp only [Profile.tail, BoundedFamily.supremum, hb, ciSup_const]74  have hc := z.property75  rw [hA, hB] at hc76  norm_num at hc7778theorem fixedPointFree_delay [WellFoundedLT ι] [WellFoundedLT κ] (z : TwoProfile ι κ) :79    z.delay ≠ z := by80  intro h81  apply no_subsolution z82  exact h.ge8384end Delay85end TwoProfile86end BFPP

SHA-256