OAI/NumberTheory/Ostmann/Construction/SeparatedPhasePacking.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.centeredPhaseBin line 12
2. theorem OAI.Ostmann.same_sign_abs_difference line 15
3. theorem OAI.Ostmann.centeredPhaseBin_injective line 26
4. theorem OAI.Ostmann.separated_phase_weight_sum line 54

   Source documentation

   Each signed distance bin contains at most one point. The zero bin costs N; all other bins cost r/k. This is the finite harmonic estimate needed for one rational-approximation block.

   theorem separated_phase_weight_sum {ι : Type*} (S : Finset ι) (f w : ι → ℝ)
       (r : ℕ) (N : ℝ) (hr : 0 < r) (hN : 0 ≤ N)
       (hsize : ∀ i ∈ S, |f i| ≤ 1 / 2)
       (hsep : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → 1 / (2 * (r : ℝ)) ≤ |f i - f j|)
       (hw : ∀ i ∈ S, 0 ≤ w i)
       (hupper : ∀ i ∈ S, w i ≤ N)
       (hdist : ∀ i ∈ S, 2 * |f i| * w i ≤ 1) :
       ∑ i ∈ S, w i ≤
         2 * ∑ k ∈ Finset.range (r + 1), if k = 0 then N else (r : ℝ) / k := by
   …