DensityMomentBridge.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.densityDivisorCount_eq_truncated line 13
Source documentation
The density descent and the arithmetic moment use exactly the same count.
```
theorem densityDivisorCount_eq_truncated (X : ℝ) (n : ℕ) :
    densityDivisorCount X n = (truncatedDivisorCount X n : ℝ) := rfl
```
Mentions: OAI.Problem337.densityDivisorCount, OAI.Problem337.truncatedDivisorCount
def OAI.Problem337.densityMomentParameter line 17
Source documentation
A common exponential size parameter for cutoffs and translated divisors.
```
def densityMomentParameter (DM : ℝ) : ℝ := 8 * (DM + 2) + DM + 1
```
theorem OAI.Problem337.densityMomentParameter_ge_one line 19

theorem OAI.Problem337.residue_level_moment_window line 25

Source documentation

Each nonterminal geometric level is inside the divisor-moment window.

theorem residue_level_moment_window
    {DM S m η : ℝ} (hDM : 1 < DM) (hS : 0 ≤ S)
    (hm : 0 < m) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
    (hmlo : S / (2 * Real.log S) ≤ m)
    {j : ℕ} (hj : j < ResidueLevels.depth ((DM + 2) * S) m η) :
    S / (2 * Real.log S) ≤
        Real.log (ResidueLevels.level ((DM + 2) * S) m η j) ∧
    Real.log (ResidueLevels.level ((DM + 2) * S) m η j) ≤
        densityMomentParameter DM * S ∧
    Real.sqrt (ResidueLevels.level ((DM + 2) * S) m η j) ≤
        ResidueLevels.level ((DM + 2) * S) m η (j + 1) ∧
    ResidueLevels.level ((DM + 2) * S) m η (j + 1) ≤
…

Mentions: OAI.Problem337.ResidueLevels.depth, OAI.Problem337.ResidueLevels.level, OAI.Problem337.densityMomentParameter

theorem OAI.Problem337.residue_level_shift_bound line 52

Source documentation

The changing factor and any divisor of the common denominator give a shift with the same fixed exponential parameter, uniformly in the level.

theorem residue_level_shift_bound
    {DM S m η : ℝ} (_hDM : 1 < DM) (hS : 0 ≤ S)
    {C M t : ℕ} (hCpos : 0 < C) (hMpos : 0 < M)
    (hC : (C : ℝ) ≤ Real.exp (8 * (DM + 2) * S))
    (hM : (M : ℝ) ≤ Real.exp (DM * S)) (ht : t ∣ M) (j : ℕ) :
    ((ResidueLevels.factor ((DM + 2) * S) m η S C j * t : ℕ) : ℝ) ≤
      Real.exp (densityMomentParameter DM * S) := by
…

Mentions: OAI.Problem337.ResidueLevels.factor, OAI.Problem337.densityMomentParameter

theorem OAI.Problem337.residue_level_moment_of_uniform line 79

Source documentation

Pointwise adapter from the uniform arithmetic estimate to the exact shifted-moment field consumed by DensityResidueFamily.

theorem residue_level_moment_of_uniform
    {DM S m η r : ℝ} (hDM : 1 < DM) (hS : 0 ≤ S)
    (hm : 0 < m) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
    (hmlo : S / (2 * Real.log S) ≤ m)
    (hmoment : ∀ (X Y : ℝ) (N : ℕ),
      S / (2 * Real.log S) ≤ Real.log X →
      Real.log X ≤ densityMomentParameter DM * S →
      Real.sqrt X ≤ Y → Y ≤ X →
      (N : ℝ) ≤ Real.exp (densityMomentParameter DM * S) →
      (∑ h ∈ Finset.Icc 1 ⌊Y⌋₊,
        (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤
          Y * Real.exp (S ^ (1 / 4 : ℝ)))
…

Mentions: OAI.Problem337.densityMomentParameter, OAI.Problem337.truncatedDivisorCount

theorem OAI.Problem337.eventually_residue_level_moment_of_uniform line 108

Source documentation

One eventual scalar moment theorem supplies every level and divisor simultaneously. The threshold does not depend on C, M, j, or t.

theorem eventually_residue_level_moment_of_uniform
    (DM η r : ℝ) (hDM : 1 < DM) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
    (hmoment : ∀ᶠ S : ℝ in atTop, ∀ (X Y : ℝ) (N : ℕ),
      S / (2 * Real.log S) ≤ Real.log X →
      Real.log X ≤ densityMomentParameter DM * S →
      Real.sqrt X ≤ Y → Y ≤ X →
      (N : ℝ) ≤ Real.exp (densityMomentParameter DM * S) →
      (∑ h ∈ Finset.Icc 1 ⌊Y⌋₊,
        (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤
          Y * Real.exp (S ^ (1 / 4 : ℝ))) :
    ∀ᶠ S : ℝ in atTop, ∀ C M : ℕ, 0 < C → 0 < M →
      (C : ℝ) ≤ Real.exp (8 * (DM + 2) * S) →
…

Mentions: OAI.Problem337.densityMomentParameter, OAI.Problem337.truncatedDivisorCount