ProfileGeometry.lean

1import BFPP.Profiles2import Mathlib.Analysis.Convex.Basic3import Mathlib.Tactic.Ring45/-! # Closedness and convexity of the increasing-profile domain -/67namespace BFPP89set_option autoImplicit false1011open Set1213universe u14variable {ι : Type u} [LinearOrder ι] [OrderBot ι]1516private theorem isClosed_forall {X : Type*} {J : Sort*} [TopologicalSpace X]17    {p : J → X → Prop} (h : ∀ j, IsClosed {x | p j x}) :18    IsClosed {x | ∀ j, p j x} := by19  simpa only [Set.ofPred_forall] using isClosed_iInter h2021theorem profileSet_isClosed : IsClosed (profileSet ι) := by22  have heval (i : ι) : Continuous (fun f : BoundedFamily ι => f i) :=23    (BoundedFamily.evaluation_nonexpansive i).continuous24  have hmono : IsClosed {f : BoundedFamily ι | Monotone f} :=25    isClosed_forall fun i => isClosed_forall fun j =>26      isClosed_forall fun (_h : i ≤ j) => isClosed_le (heval i) (heval j)27  exact (isClosed_eq (heval ⊥) continuous_const).inter28    (hmono.inter (isClosed_forall fun i => isClosed_Icc.preimage (heval i)))2930theorem profileSet_convex : Convex ℝ (profileSet ι) := by31  intro x hx y hy r s hr hs hrs32  change (r * x ⊥ + s * y ⊥ = 0) ∧33    Monotone (fun i => r * x i + s * y i) ∧34    ∀ i, r * x i + s * y i ∈ Icc (0 : ℝ) 235  refine ⟨?_, ?_, ?_⟩36  · rw [hx.1, hy.1]37    ring38  · intro i j hij39    exact add_le_add (mul_le_mul_of_nonneg_left (hx.2.1 hij) hr)40      (mul_le_mul_of_nonneg_left (hy.2.1 hij) hs)41  · intro i42    constructor43    · exact add_nonneg (mul_nonneg hr (hx.2.2 i).1) (mul_nonneg hs (hy.2.2 i).1)44    · have h₁ := mul_le_mul_of_nonneg_left (hx.2.2 i).2 hr45      have h₂ := mul_le_mul_of_nonneg_left (hy.2.2 i).2 hs46      linarith4748theorem Profile.norm_le_two (a : Profile ι) : ‖a.val‖ ≤ 2 := by49  letI : TopologicalSpace ι := ⊥50  apply (BoundedContinuousFunction.norm_le (by norm_num : (0 : ℝ) ≤ 2)).251  intro i52  rw [Real.norm_eq_abs, abs_of_nonneg (a.nonneg i)]53  exact a.le_two i5455noncomputable def Profile.mix (a b : Profile ι) (r s : ℝ)56    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) : Profile ι :=57  ⟨r • a.val + s • b.val, profileSet_convex a.property b.property hr hs hrs⟩5859@[simp] theorem Profile.mix_apply (a b : Profile ι) (r s : ℝ)60    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) (i : ι) :61    (a.mix b r s hr hs hrs).val i = r * a.val i + s * b.val i := rfl6263theorem Profile.tail_mix (a b : Profile ι) (r s : ℝ)64    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) :65    (a.mix b r s hr hs hrs).tail = r * a.tail + s * b.tail := by66  apply le_antisymm67  · apply ciSup_le68    intro i69    exact add_le_add (mul_le_mul_of_nonneg_left (a.le_tail i) hr)70      (mul_le_mul_of_nonneg_left (b.le_tail i) hs)71  · apply le_of_forall_pos_le_add72    intro ε hε73    obtain ⟨i, hi⟩ := exists_lt_of_lt_ciSup74      (show a.tail - ε < ⨆ i, a.val i by change a.tail - ε < a.tail; linarith)75    obtain ⟨j, hj⟩ := exists_lt_of_lt_ciSup76      (show b.tail - ε < ⨆ j, b.val j by change b.tail - ε < b.tail; linarith)77    have ha : a.tail - ε ≤ a.val (max i j) :=78      hi.le.trans (a.monotone (le_max_left i j))79    have hb : b.tail - ε ≤ b.val (max i j) :=80      hj.le.trans (b.monotone (le_max_right i j))81    have h₁ := mul_le_mul_of_nonneg_left ha hr82    have h₂ := mul_le_mul_of_nonneg_left hb hs83    have h₃ := (a.mix b r s hr hs hrs).le_tail (max i j)84    rw [Profile.mix_apply] at h₃85    have hεsum : (r + s) * ε = ε := by rw [hrs, one_mul]86    nlinarith8788/-- A concrete profile used to witness nonemptiness of the coefficient domain. -/89noncomputable def Profile.stepOne : Profile ι := by90  classical91  let f : BoundedFamily ι := BoundedFamily.ofBound92    (fun i => if i = ⊥ then 0 else 1) 1 (fun i => by split_ifs <;> norm_num)93  refine ⟨f, ?_, ?_, ?_⟩94  · simp [f]95  · intro i j hij96    change (if i = ⊥ then (0 : ℝ) else 1) ≤ (if j = ⊥ then 0 else 1)97    by_cases hi : i = ⊥98    · rw [if_pos hi]99      split_ifs <;> norm_num100    · have hj : j ≠ ⊥ := fun h => hi (bot_unique (h ▸ hij))101      simp [hi, hj]102  · intro i103    change (if i = ⊥ then (0 : ℝ) else 1) ∈ Icc 0 2104    split_ifs <;> norm_num105106theorem Profile.tail_stepOne [NoMaxOrder ι] : (Profile.stepOne : Profile ι).tail = 1 := by107  classical108  apply le_antisymm109  · apply ciSup_le110    intro i111    change (if i = ⊥ then (0 : ℝ) else 1) ≤ 1112    split_ifs <;> norm_num113  · obtain ⟨i, hi⟩ := exists_gt (⊥ : ι)114    have h := (Profile.stepOne : Profile ι).le_tail i115    change (if i = ⊥ then (0 : ℝ) else 1) ≤ _ at h116    simpa [ne_of_gt hi] using h117118end BFPP

SHA-256