HighResidueDistribution.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.residueFourierAverage line 15
Source documentation
The ordinary normalized exponential sum, defined also at modulus zero. All residue conclusions below explicitly require a positive modulus.
```
def residueFourierAverage {Ω : Type*} [Fintype Ω]
    (A : Ω → ℕ) (u l : ℕ) : ℂ :=
…
```

theorem OAI.Problem337.ceiling_remainder_count_of_exp_average line 23

Source documentation

An automatic-scale version of the positive exponential-average ceiling count. The index type, rather than the image, counts repeated entries.

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

Mentions: OAI.Problem337.residueFourierAverage

def OAI.Problem337.highResidueExceptions line 37
Source documentation
The Fourier exception set for the deterministic high levels.
```
def highResidueExceptions {Ω : Type*} [Fintype Ω]
    (U : Finset ℕ) (A : Ω → ℕ) (m : ℝ) : Finset ℕ := by
…
```

theorem OAI.Problem337.highResidueExceptions_card_bound line 45

Source documentation

The exact frequency-union exponent is -9m/1000. This is stronger than the -m/1000 exception budget required by density descent.

theorem highResidueExceptions_card_bound {Ω : Type*} [Fintype Ω]
    (U : Finset ℕ) (A : Ω → ℕ) (m X : ℝ) (hX : 0 ≤ X)
    (hmoment : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊Real.exp (m / 2500)⌋₊ →
      (∑ u ∈ U, ‖residueFourierAverage A u l‖ ^ 2) ≤ X * Real.exp (-m / 100)) :
    ((highResidueExceptions U A m).card : ℝ) ≤ X * Real.exp (-9 * m / 1000) := by
…

Mentions: OAI.Problem337.residueFourierAverage, OAI.Problem337.highResidueExceptions

theorem OAI.Problem337.highResidueExceptions_fourier line 81

Source documentation

Outside the explicit exception set, every frequency needed by the cyclic localization theorem satisfies the correct cubed-density bound.

theorem highResidueExceptions_fourier {Ω : Type*} [Fintype Ω]
    (U : Finset ℕ) (A : Ω → ℕ) (m : ℝ) {u : ℕ}
    (hu : u ∈ U) (hgood : u ∉ highResidueExceptions U A m) :
    ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / Real.exp (-m / 10000) ^ 4⌋₊ →
      ‖residueFourierAverage A u l‖ ≤ Real.exp (-m / 10000) ^ 3 := by
…

Mentions: OAI.Problem337.highResidueExceptions, OAI.Problem337.residueFourierAverage

theorem OAI.Problem337.high_level_residues_of_second_moments line 106

Source documentation

Deterministic high-level residue distribution from its normalized second moments. No cancellation or discrepancy hypothesis is hidden in the output: the only input still needed is precisely the displayed second-moment bound.

theorem high_level_residues_of_second_moments {Ω : Type*} [Fintype Ω]
    (U : Finset ℕ) (A : Ω → ℕ) (m X : ℝ)
    (hm : 0 ≤ m) (hX : 0 ≤ X)
    (hsmall : Real.exp (-m / 10000) ≤ 1 / 65536)
    (hupos : ∀ u ∈ U, 0 < u) (hubound : ∀ u ∈ U, (u : ℝ) ≤ X)
    (hmoment : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊Real.exp (m / 2500)⌋₊ →
      (∑ u ∈ U, ‖residueFourierAverage A u l‖ ^ 2) ≤ X * Real.exp (-m / 100)) :
    ∃ E : Finset ℕ, E ⊆ U ∧ (E.card : ℝ) ≤ X * Real.exp (-m / 1000) ∧
      ∀ u ∈ U, u ∉ E →
        (Real.exp (-m / 10000) / 2) * (Fintype.card Ω : ℝ) ≤
          ((Finset.univ.filter (fun ω =>
            ((u * ⌈(A ω : ℚ) / (u : ℚ)⌉₊ - A ω : ℕ) : ℝ) ≤
…

Mentions: OAI.Problem337.residueFourierAverage

theorem OAI.Problem337.rational_ceiling_residue_lt_iff_fract_lt line 145
Source documentation
The rational-ceiling convention in cyclic counts and the real-ceiling convention in geometric descent specify exactly the same least residue.
```
theorem rational_ceiling_residue_lt_iff_fract_lt (u A : ℕ) (hu : 0 < u) (δ : ℝ) :
    ((u * ⌈(A : ℚ) / (u : ℚ)⌉₊ - A : ℕ) : ℝ) < δ * u ↔
      Int.fract (-(A : ℝ) / u) < δ := by
…
```

theorem OAI.Problem337.fractional_residue_count_of_exp_average line 155

Source documentation

The direct fractional-part count needed by geometric residue families.

theorem fractional_residue_count_of_exp_average {Ω : Type*} [Fintype Ω]
    (A : Ω → ℕ) (u : ℕ) (hu : 0 < u) (δ : ℝ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536)
    (hfourier : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊1 / δ ^ 4⌋₊ →
      ‖residueFourierAverage A u l‖ ≤ δ ^ 3) :
    (δ / 2) * (Fintype.card Ω : ℝ) ≤
      ((Finset.univ.filter (fun ω => Int.fract (-(A ω : ℝ) / u) < δ)).card : ℝ) := by
…

Mentions: OAI.Problem337.residueFourierAverage

theorem OAI.Problem337.high_level_fractional_residues_of_second_moments line 169

Source documentation

High-level distribution in exactly the fractional-part convention used by geometric raw-density packaging. The exceptional set is independent of the chosen residue index, and multiplicities are retained.

theorem high_level_fractional_residues_of_second_moments
    {Ω : Type*} [Fintype Ω] (U : Finset ℕ) (A : Ω → ℕ) (m X : ℝ)
    (hm : 0 ≤ m) (hX : 0 ≤ X)
    (hsmall : Real.exp (-m / 10000) ≤ 1 / 65536)
    (hupos : ∀ u ∈ U, 0 < u)
    (hmoment : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊Real.exp (m / 2500)⌋₊ →
      (∑ u ∈ U, ‖residueFourierAverage A u l‖ ^ 2) ≤ X * Real.exp (-m / 100)) :
    ∃ E : Finset ℕ, E ⊆ U ∧ (E.card : ℝ) ≤ X * Real.exp (-m / 1000) ∧
      ∀ u ∈ U, u ∉ E →
        (Real.exp (-m / 10000) / 2) * (Fintype.card Ω : ℝ) ≤
          ((Finset.univ.filter (fun ω =>
            Int.fract (-(A ω : ℝ) / u) < Real.exp (-m / 10000))).card : ℝ) := by
…

Mentions: OAI.Problem337.residueFourierAverage

theorem OAI.Problem337.high_level_fractional_residues_finset line 195

Source documentation

Finset-indexed form, matching the deterministic second-moment interface. Repeated values of A remain distinct indices of T.

theorem high_level_fractional_residues_finset
    {ι : Type*} (T : Finset ι) (A : ι → ℕ) (U : Finset ℕ) (m X : ℝ)
    (hm : 0 ≤ m) (hX : 0 ≤ X)
    (hsmall : Real.exp (-m / 10000) ≤ 1 / 65536)
    (hupos : ∀ u ∈ U, 0 < u)
    (hmoment : ∀ l : ℕ, 1 ≤ l → l ≤ ⌊Real.exp (m / 2500)⌋₊ →
      (∑ u ∈ U, ‖(∑ i ∈ T, Complex.exp
        (2 * Real.pi * Complex.I * (l * A i : ℕ) / (u : ℂ))) /
          (T.card : ℂ)‖ ^ 2) ≤ X * Real.exp (-m / 100)) :
    ∃ E : Finset ℕ, E ⊆ U ∧ (E.card : ℝ) ≤ X * Real.exp (-m / 1000) ∧
      ∀ u ∈ U, u ∉ E →
        (Real.exp (-m / 10000) / 2) * (T.card : ℝ) ≤
…

theorem OAI.Problem337.eventually_high_residue_localization_scale line 233
Source documentation
The only small-density cutoff in the finite discrepancy argument holds uniformly at the canonical prime-product scale.
```
theorem eventually_high_residue_localization_scale :
    ∀ᶠ S : ℝ in atTop,
      Real.exp (-(ResidueLevels.scale S : ℝ) / 10000) ≤ 1 / 65536 := by
…
```
Mentions: OAI.Problem337.ResidueLevels.scale