FejerBudget.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.cyclic_interval_floor_budget line 8

Source documentation

Rounding the inner cyclic interval leaves fixed proportional margins.

theorem cyclic_interval_floor_budget (δ : ℝ) (q : ℕ)
    (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hscale : 128 ≤ δ * q) :
    let d := ⌊δ * q / 8⌋₊
…

theorem OAI.Problem337.fejer_degree_floor_budget line 43
Source documentation
A low-degree kernel simultaneously has small leakage and Fourier error.
```
theorem fejer_degree_floor_budget (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536) :
    let h := ⌊1 / (64 * δ ^ 3)⌋₊
…
```

theorem OAI.Problem337.fejer_degree_frequency_bound line 89

Source documentation

The chosen degree uses only the prescribed low frequencies.

theorem fejer_degree_frequency_bound (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536) :
    ⌊1 / (64 * δ ^ 3)⌋₊ ≤ ⌊1 / δ ^ 4⌋₊ := by
…

theorem OAI.Problem337.fejer_localization_budget line 99

Source documentation

The three error budgets leave at least half the target interval mass.

theorem fejer_localization_budget (δ mass inner error leakage : ℝ)
    (hδ : 0 ≤ δ) (hinner : 11 * δ / 16 ≤ inner)
    (herror : error ≤ δ / 32) (hleakage : leakage ≤ δ / 8)
    (hmass : inner - error - leakage ≤ mass) : δ / 2 ≤ mass := by
…