RationalDiscrepancy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.rational_small_interval_of_fourier line 15

Source documentation

Sharp lower-interval discrepancy for rational phases, using a sufficiently large common cyclic modulus. There is no common-denominator hypothesis and there are no modulus-size side conditions on the conclusion.

theorem rational_small_interval_of_fourier {Ω : Type*} [Fintype Ω]
    (x : Ω → ℚ) (hx0 : ∀ ω, 0 ≤ x ω) (hx1 : ∀ ω, x ω < 1) (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536)
    (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
      ‖∑ ω : Ω, (Circle.exp (2 * Real.pi * (x ω : ℝ)) : ℂ) ^ l‖ ≤
        (Fintype.card Ω : ℝ) * δ ^ 3) :
    (δ / 2) * (Fintype.card Ω : ℝ) ≤
      ((Finset.univ.filter (fun ω => (x ω : ℝ) < δ)).card : ℝ) := by
…

theorem OAI.Problem337.rational_small_interval_of_fourier_finset line 44

Source documentation

Finset-indexed rational discrepancy, including an empty sample set.

theorem rational_small_interval_of_fourier_finset {Ω : Type*}
    (samples : Finset Ω) (x : Ω → ℚ)
    (hx0 : ∀ ω ∈ samples, 0 ≤ x ω) (hx1 : ∀ ω ∈ samples, x ω < 1) (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536)
    (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
      ‖∑ ω ∈ samples, (Circle.exp (2 * Real.pi * (x ω : ℝ)) : ℂ) ^ l‖ ≤
        (samples.card : ℝ) * δ ^ 3) :
    (δ / 2) * (samples.card : ℝ) ≤
      ((samples.filter (fun ω => (x ω : ℝ) < δ)).card : ℝ) := by
…

theorem OAI.Problem337.eventually_rational_exponential_interval line 71

Source documentation

The sharp exponential localization form, uniform over all finite rational sample families once the scale is sufficiently large.

theorem eventually_rational_exponential_interval {Ω : Type*}
    (η : ℝ) (hη : 0 < η) :
    ∀ᶠ w : ℝ in Filter.atTop, ∀ (samples : Finset Ω) (x : Ω → ℚ),
      (∀ ω ∈ samples, 0 ≤ x ω) → (∀ ω ∈ samples, x ω < 1) →
      (∀ l : ℕ, 1 ≤ l → l ≤ ⌊Real.exp (4 * η * w)⌋₊ →
        ‖∑ ω ∈ samples, (Circle.exp (2 * Real.pi * (x ω : ℝ)) : ℂ) ^ l‖ ≤
          (samples.card : ℝ) * Real.exp (-3 * η * w)) →
      (Real.exp (-η * w) / 2) * (samples.card : ℝ) ≤
        ((samples.filter (fun ω => (x ω : ℝ) < Real.exp (-η * w))).card : ℝ) := by
…