HighWeightResidueMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Residue-uniform high-weight mass via the small half kernels

theorem OAI.Ostmann.half_kernel_residue_mass line 14

Source documentation

The half-kernel construction converts the mass in one residue class into a reciprocal squarefree sum. Its fibers are controlled uniformly in the residue.

theorem half_kernel_residue_mass (S : Finset ℕ) (N L a : ℕ)
    (hL : 0 < L) (hsize : 2 * L ^ 2 ≤ N)
    (hS : ∀ s ∈ S, Squarefree s)
    (hrange : ∀ s ∈ S, s ∈ Finset.Ioc N (2 * N))
    (hres : ∀ s ∈ S, Nat.ModEq L s a)
    (hcop : ∀ s ∈ S, L.Coprime s) (u : ℝ) (hu : 1 ≤ u) :
    (∑ s ∈ S, u ^ s.primeFactors.card) ≤
      (2 * u * N / L) * ∑ r ∈ S.image smallHalfKernel, (u ^ 2) ^ r.primeFactors.card / (r : ℝ) := by
…

Mentions: OAI.Ostmann.smallHalfKernel

theorem OAI.Ostmann.high_weight_residue_mass line 63

Source documentation

Rankin's parameter bounds the residue mass with its half-kernel, congruence and multiplicity conditions.

theorem high_weight_residue_mass (S P : Finset ℕ) (N L a b : ℕ)
    (hL : 0 < L) (hsize : 2 * L ^ 2 ≤ N)
    (hS : ∀ s ∈ S, Squarefree s)
    (hrange : ∀ s ∈ S, s ∈ Finset.Ioc N (2 * N))
    (hres : ∀ s ∈ S, Nat.ModEq L s a) (hcop : ∀ s ∈ S, L.Coprime s)
    (hP : ∀ s ∈ S, (smallHalfKernel s).primeFactors ⊆ P)
    (hb : ∀ s ∈ S, b ≤ (smallHalfKernel s).primeFactors.card)
    (u t : ℝ) (hu : 1 ≤ u) (ht : 1 ≤ t) :
    (∑ s ∈ S, u ^ s.primeFactors.card) ≤
      (2 * u * N / L) * (t ^ b)⁻¹ *
        Real.exp (u ^ 2 * t * ∑ p ∈ P, (p : ℝ)⁻¹) := by
…

Mentions: OAI.Ostmann.smallHalfKernel