AngularBinTransfer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Angular-bin transfer for a separated list

These are the quantitative bin-width and enlargement calculations used after transferring a popularity witness to a reference line in §6.

theorem OAI.LipschitzHilbert.AngularBins.baseBin_width_le_relative line 16
theorem OAI.LipschitzHilbert.AngularBins.baseBin_width_lt_separation line 27

theorem OAI.LipschitzHilbert.AngularBins.separated_annulus_bins_injective line 37

Source documentation

The bins chosen for a separated list are distinct, since their widths are at most rho/B with B>1.

theorem separated_annulus_bins_injective {ι : Type*} (s : ℝ) {M : ℕ} (hM : 0 < M)
    {B rho : ℝ} (hB : 1 < B) (hrho : 0 < rho) (hMB : (M : ℝ) = B ^ 2)
    (frequency : ι → ℝ) (bin : ι → Bin M)
    (hsep : PhaseCombinatorics.Separated frequency rho)
    (hmem : ∀ i, frequency i ∈ baseBin s (bin i))
    (hrelative : ∀ i, |frequency i - s| ≤ B * rho) : Function.Injective bin :=
…

Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.AngularBins.baseBin

theorem OAI.LipschitzHilbert.AngularBins.enlargedBin_mono line 46
theorem OAI.LipschitzHilbert.AngularBins.transferred_slope_mem_enlarged line 60
Source documentation
The transferred witness error is at most (c0+1) Delta/M. The annulus relation Delta<2*2^h makes a fixed concentric enlargement sufficient for every scale and every separated list.
```
theorem transferred_slope_mem_enlarged (s : ℝ) {M : ℕ} (hM : 0 < M)
    {c0 c a a' : ℝ} (hc0 : 0 ≤ c0) (hc : 4 * (c0 + 1) + 1 ≤ c)
    {b : Bin M} (ha : a ∈ baseBin s b)
    (herror : |a' - a| ≤ (c0 + 1) * |a - s| / M) :
    a' ∈ enlargedBin s c b := by
…
```
Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.AngularBins.baseBin, OAI.LipschitzHilbert.AngularBins.enlargedBin