CyclicDiscrepancy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.CyclicSmoothing.initial_interval_count_of_kernel_mean line 15

Source documentation

The geometric and counting part of cyclic discrepancy. The sampled spectral-mean input is separated from the exact kernel normalization.

theorem initial_interval_count_of_kernel_mean {q h d : ℕ} [NeZero q]
    {Ω : Type*} (samples : Finset Ω) (x : Ω → ZMod q) (ε : ℝ)
    (hh : 0 < h) (hhq : h ≤ q) (hd : 0 < d) (hdq : 7 * d < q)
    (hmean : ∀ y : ZMod q,
      (samples.card : ℝ) * (1 - ((h : ℝ) - 1) * ε) ≤
        ∑ ω ∈ samples, GeometricKernel.kernel h (ZMod.stdAddChar (x ω - y))) :
    (samples.card : ℝ) *
      (((6 * d + 1 : ℕ) : ℝ) / q -
        (((6 * d + 1 : ℕ) : ℝ) / q) * ((h : ℝ) - 1) * ε -
        (((6 * d + 1 : ℕ) : ℝ) / q) / (4 * (h : ℝ) * ((d : ℝ) / q)^2)) ≤
      ((samples.filter (fun ω => (x ω).val < 8 * d)).card : ℝ) := by
…

Mentions: OAI.Problem337.GeometricKernel.kernel

theorem OAI.Problem337.CyclicSmoothing.cyclic_small_interval_of_kernel_mean line 78

Source documentation

With the explicit low-degree choice, the smoothing errors leave half of the desired interval mass. This lemma isolates the sampled kernel mean.

theorem cyclic_small_interval_of_kernel_mean {q : ℕ} [NeZero q]
    {Ω : Type*} (samples : Finset Ω) (x : Ω → ZMod q) (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536) (hscale : 128 ≤ δ * q)
    (hdegree : ⌊1 / (64 * δ ^ 3)⌋₊ ≤ q)
    (hmean : ∀ y : ZMod q,
      (samples.card : ℝ) * (1 - ((⌊1 / (64 * δ ^ 3)⌋₊ : ℝ) - 1) * δ ^ 3) ≤
        ∑ ω ∈ samples, GeometricKernel.kernel ⌊1 / (64 * δ ^ 3)⌋₊
          (ZMod.stdAddChar (x ω - y))) :
    (δ / 2) * (samples.card : ℝ) ≤
      ((samples.filter (fun ω => ((x ω).val : ℝ) < δ * q)).card : ℝ) := by
…

Mentions: OAI.Problem337.GeometricKernel.kernel

theorem OAI.Problem337.CyclicSmoothing.cyclic_small_interval_of_fourier line 146

Source documentation

Genuine finite cyclic low-frequency discrepancy, with no sampled-kernel hypothesis remaining. Repeated samples are allowed.

theorem cyclic_small_interval_of_fourier {q : ℕ} [NeZero q]
    {Ω : Type*} [Fintype Ω] (x : Ω → ZMod q) (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536) (hscale : 128 ≤ δ * q)
    (hdegree : ⌊1 / (64 * δ ^ 3)⌋₊ ≤ q)
    (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
      ‖∑ ω : Ω, ZMod.stdAddChar ((l : ZMod q) * x ω)‖ ≤
        (Fintype.card Ω : ℝ) * δ ^ 3) :
    (δ / 2) * (Fintype.card Ω : ℝ) ≤
      ((Finset.univ.filter (fun ω => ((x ω).val : ℝ) < δ * q)).card : ℝ) := by
…

theorem OAI.Problem337.CyclicSmoothing.cyclic_small_interval_of_fourier_finset line 175

Source documentation

Finset-indexed version of the same discrepancy bound.

theorem cyclic_small_interval_of_fourier_finset {q : ℕ} [NeZero q]
    {Ω : Type*} (samples : Finset Ω) (x : Ω → ZMod q) (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536) (hscale : 128 ≤ δ * q)
    (hdegree : ⌊1 / (64 * δ ^ 3)⌋₊ ≤ q)
    (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
      ‖∑ ω ∈ samples, ZMod.stdAddChar ((l : ZMod q) * x ω)‖ ≤
        (samples.card : ℝ) * δ ^ 3) :
    (δ / 2) * (samples.card : ℝ) ≤
      ((samples.filter (fun ω => ((x ω).val : ℝ) < δ * q)).card : ℝ) := by
…