OAI/NumberTheory/EgyptianFractions/CyclicCeilingCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ceiling_remainder_count_of_fourier line 12

   Source documentation

   Positive exponential cancellation supplies many small natural ceiling remainders, with repetitions of the indexed numerators retained.

   theorem ceiling_remainder_count_of_fourier {u : ℕ} [NeZero u]
       {Ω : Type*} [Fintype Ω] (A : Ω → ℕ) (δ : ℝ)
       (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536) (hscale : 128 ≤ δ * u)
       (hdegree : ⌊1 / (64 * δ ^ 3)⌋₊ ≤ u)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
         ‖∑ ω : Ω, Complex.exp
           (2 * Real.pi * Complex.I * (l * A ω : ℕ) / (u : ℂ))‖ ≤
             (Fintype.card Ω : ℝ) * δ ^ 3) :
       (δ / 2) * (Fintype.card Ω : ℝ) ≤
         ((Finset.univ.filter (fun ω =>
           ((u * ⌈(A ω : ℚ) / (u : ℚ)⌉₊ - A ω : ℕ) : ℝ) < δ * u)).card : ℝ) := by
   …

2. theorem OAI.Problem337.ceiling_remainder_count_of_fourier_average line 32

   Source documentation

   The same counting conclusion from normalized Fourier averages.

   theorem ceiling_remainder_count_of_fourier_average {u : ℕ} [NeZero u]
       {Ω : Type*} [Fintype Ω] (A : Ω → ℕ) (δ : ℝ)
       (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536) (hscale : 128 ≤ δ * u)
       (hdegree : ⌊1 / (64 * δ ^ 3)⌋₊ ≤ u)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
         ‖(∑ ω : Ω, Complex.exp
           (2 * Real.pi * Complex.I * (l * A ω : ℕ) / (u : ℂ))) /
             (Fintype.card Ω : ℂ)‖ ≤ δ ^ 3) :
       (δ / 2) * (Fintype.card Ω : ℝ) ≤
         ((Finset.univ.filter (fun ω =>
           ((u * ⌈(A ω : ℚ) / (u : ℚ)⌉₊ - A ω : ℕ) : ℝ) < δ * u)).card : ℝ) := by
   …

3. theorem OAI.Problem337.ceiling_remainder_count_of_character_expect line 59

   Source documentation

   Direct finite-average character interface for the random-product second moment route; no conversion to real fractional parts is required.

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

4. theorem OAI.Problem337.ceiling_remainder_count_of_character_expect_automatic line 76

   Source documentation

   Cancellation forces its own modulus-size conditions, so the direct ceiling-remainder count has no separate scale or degree hypothesis.

   theorem ceiling_remainder_count_of_character_expect_automatic {u : ℕ} [NeZero u]
       {Ω : Type*} [Fintype Ω] (A : Ω → ℕ) (δ : ℝ)
       (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
         ‖𝔼 ω : Ω, ZMod.stdAddChar ((l : ZMod u) * (A ω : ZMod u))‖ ≤ δ ^ 3) :
       (δ / 2) * (Fintype.card Ω : ℝ) ≤
         ((Finset.univ.filter (fun ω =>
           ((u * ⌈(A ω : ℚ) / (u : ℚ)⌉₊ - A ω : ℕ) : ℝ) < δ * u)).card : ℝ) := by
   …