FiniteSynthesis.lean

1import Mathlib.Algebra.Order.Archimedean.Real.Basic2import Mathlib.Algebra.BigOperators.Group.List.Basic3import Mathlib.Data.List.Sort4import Mathlib.Data.Finset.Sort5import Mathlib.Algebra.BigOperators.Group.Finset.Basic6import Mathlib.Tactic.Linarith7import Mathlib.Tactic.Ring89/-! # The finite positive-synthesis estimate1011For an increasing sequence of weights in `[0,W]`, bounds on every tail sum of12the coefficients give the same bounds, scaled by `W`, on the weighted sum.13This is the finite estimate behind the positive operator extension.14-/1516namespace BFPP1718set_option autoImplicit false1920universe u21variable {ι : Type u}2223def TailSumBounds (l : List ι) (c : ι → ℝ) (m M : ℝ) : Prop :=24  ∀ t : List ι, t <:+ l → m ≤ (t.map c).sum ∧ (t.map c).sum ≤ M2526theorem sum_shift_weights (l : List ι) (c w : ι → ℝ) (b : ℝ) :27    (l.map (fun i => c i * (w i - b))).sum =28      (l.map (fun i => c i * w i)).sum - (l.map c).sum * b := by29  induction l with30  | nil => simp31  | cons a l ih =>32    simp only [List.map_cons, List.sum_cons, ih]33    ring3435theorem finite_synthesis_bounds [Preorder ι] (l : List ι) (c w : ι → ℝ)36    (m M W : ℝ) (hW : 0 ≤ W) (hs : l.Pairwise (· ≤ ·))37    (hw : Monotone w) (hb : ∀ i ∈ l, 0 ≤ w i ∧ w i ≤ W)38    (ht : TailSumBounds l c m M) :39    m * W ≤ (l.map (fun i => c i * w i)).sum ∧40      (l.map (fun i => c i * w i)).sum ≤ M * W := by41  induction l generalizing w W with42  | nil =>43    have hzero := ht [] (by simp)44    simp only [List.map_nil, List.sum_nil] at hzero ⊢45    exact ⟨mul_nonpos_of_nonpos_of_nonneg hzero.1 hW, mul_nonneg hzero.2 hW⟩46  | cons a l ih =>47    have hhead := hb a (List.mem_cons_self ..)48    have hp := List.pairwise_cons.mp hs49    have htail : TailSumBounds l c m M := by50      intro t ht'51      exact ht t (ht'.trans (List.suffix_cons a l))52    have hb' : ∀ i ∈ l, 0 ≤ w i - w a ∧ w i - w a ≤ W - w a := by53      intro i hi54      have hwi := hb i (List.mem_cons_of_mem a hi)55      exact ⟨sub_nonneg.mpr (hw (hp.1 i hi)), sub_le_sub_right hwi.2 _⟩56    have hm : Monotone (fun i => w i - w a) := fun _ _ hij => sub_le_sub_right (hw hij) _57    have hi := ih (fun i => w i - w a) (W - w a) (sub_nonneg.mpr hhead.2)58      hp.2 hm hb' htail59    have hall := ht (a :: l) (by simp)60    simp only [List.map_cons, List.sum_cons] at hall ⊢61    have hlow := mul_le_mul_of_nonneg_right hall.1 hhead.162    have hupp := mul_le_mul_of_nonneg_right hall.2 hhead.163    rw [sum_shift_weights] at hi64    constructor <;> nlinarith [hi.1, hi.2]6566theorem finite_synthesis_abs_bound [Preorder ι] (l : List ι) (c w : ι → ℝ)67    (C : ℝ) (hs : l.Pairwise (· ≤ ·)) (hw : Monotone w)68    (hb : ∀ i ∈ l, 0 ≤ w i ∧ w i ≤ 1)69    (ht : ∀ t : List ι, t <:+ l → |(t.map c).sum| ≤ C) :70    |(l.map (fun i => c i * w i)).sum| ≤ C := by71  have h := finite_synthesis_bounds l c w (-C) C 1 (by norm_num) hs hw hb72    (fun t htl => abs_le.mp (ht t htl))73  apply abs_le.mpr74  simpa only [mul_one] using h7576theorem finite_synthesis_nonneg [Preorder ι] (l : List ι) (c w : ι → ℝ)77    (M : ℝ) (hs : l.Pairwise (· ≤ ·)) (hw : Monotone w)78    (hb : ∀ i ∈ l, 0 ≤ w i ∧ w i ≤ 1) (ht : TailSumBounds l c 0 M) :79    0 ≤ (l.map (fun i => c i * w i)).sum := by80  have h := (finite_synthesis_bounds l c w 0 M 1 (by norm_num) hs hw hb ht).181  simpa only [zero_mul] using h8283noncomputable def stepListValue [LinearOrder ι] (l : List ι) (c : ι → ℝ) (i : ι) : ℝ :=84  (l.map (fun j => if i ≤ j then c j else 0)).sum8586theorem tailSumBounds_of_stepList [LinearOrder ι] (l : List ι) (c : ι → ℝ) (m M : ℝ)87    (hs : l.Pairwise (· < ·)) (hm : m ≤ 0) (hM : 0 ≤ M)88    (hf : ∀ i ∈ l, m ≤ stepListValue l c i ∧ stepListValue l c i ≤ M) :89    TailSumBounds l c m M := by90  induction l with91  | nil =>92    intro t ht93    have he := List.suffix_nil.mp ht94    simpa [he] using And.intro hm hM95  | cons a l ih =>96    have hp := List.pairwise_cons.mp hs97    have htail : TailSumBounds l c m M := by98      apply ih hp.299      intro i hi100      have h := hf i (List.mem_cons_of_mem a hi)101      have hia : ¬ i ≤ a := not_le.mpr (hp.1 i hi)102      simpa [stepListValue, hia] using h103    have hfirst : stepListValue (a :: l) c a = c a + (l.map c).sum := by104      have he : l.map (fun j => if a ≤ j then c j else 0) = l.map c := by105        apply List.map_congr_left106        intro j hj107        simp only [if_pos (hp.1 j hj).le]108      simp only [stepListValue, List.map_cons, if_pos le_rfl, List.sum_cons, he]109    intro t ht110    rcases List.suffix_cons_iff.mp ht with rfl | ht111    · have h := hf a (List.mem_cons_self ..)112      simpa only [hfirst, List.map_cons, List.sum_cons] using h113    · exact htail t ht114115theorem sum_map_sort [LinearOrder ι] (s : Finset ι) (f : ι → ℝ) :116    (s.sort.map f).sum = ∑ i ∈ s, f i := by117  rw [← List.sum_toFinset f (s.sort_nodup (· ≤ ·)), Finset.sort_toFinset]118119noncomputable def stepFinsetValue [LinearOrder ι] (s : Finset ι) (c : ι → ℝ) (i : ι) : ℝ :=120  ∑ j ∈ s, if i ≤ j then c j else 0121122theorem finite_synthesis_bounds_finset [LinearOrder ι] (s : Finset ι) (c w : ι → ℝ)123    (m M : ℝ) (hm : m ≤ 0) (hM : 0 ≤ M) (hw : Monotone w)124    (hb : ∀ i ∈ s, 0 ≤ w i ∧ w i ≤ 1)125    (hf : ∀ i, m ≤ stepFinsetValue s c i ∧ stepFinsetValue s c i ≤ M) :126    m ≤ ∑ i ∈ s, c i * w i ∧ (∑ i ∈ s, c i * w i) ≤ M := by127  have ht : TailSumBounds s.sort c m M := by128    apply tailSumBounds_of_stepList _ _ _ _ s.sortedLT_sort.pairwise hm hM129    intro i _hi130    simpa only [stepListValue, sum_map_sort, stepFinsetValue] using hf i131  have h := finite_synthesis_bounds s.sort c w m M 1 (by norm_num)132    (s.pairwise_sort (· ≤ ·)) hw133    (fun i hi => hb i (by simpa using hi)) ht134  simpa only [sum_map_sort, mul_one] using h135136theorem finite_synthesis_abs_bound_finset [LinearOrder ι] (s : Finset ι) (c w : ι → ℝ)137    (C : ℝ) (hC : 0 ≤ C) (hw : Monotone w)138    (hb : ∀ i ∈ s, 0 ≤ w i ∧ w i ≤ 1)139    (hf : ∀ i, |stepFinsetValue s c i| ≤ C) :140    |∑ i ∈ s, c i * w i| ≤ C := by141  apply abs_le.mpr142  exact finite_synthesis_bounds_finset s c w (-C) C (neg_nonpos.mpr hC) hC hw hb143    (fun i => abs_le.mp (hf i))144145end BFPP

SHA-256