PageKernelExclusion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the kernel family of a large Page character

def OAI.Ostmann.pageKernelExclusion line 13

theorem OAI.Ostmann.page_kernel_retention line 20

Source documentation

A kernel outside the explicit excluded family can only represent a selected Page character whose conductor is at most the retained threshold.

theorem page_kernel_retention (P : PublishedProgressionInput) (Q : ℕ) (R : ℝ)
    (d : ℤ) (χ : PrimitiveRealCharacter) (N : ℕ) (hN : 0 < N)
    (hNq : N ∣ χ.modulus) (hqN : χ.modulus ≤ 8 * N)
    (hdN : d.natAbs = N ∨ d.natAbs = 2 * N) (hqd : χ.modulus ≤ 4 * d.natAbs)
    (hout : d ∉ pageKernelExclusion P Q R)
    (e : PrimitiveRealZero) (he : selectedPageZero P Q = some e)
    (hsame : samePrimitiveRealCharacter e χ) : (e.modulus : ℝ) ≤ R := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.pageKernelExclusion, OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.selectedPageZero, OAI.Ostmann.samePrimitiveRealCharacter

theorem OAI.Ostmann.page_kernel_exclusion_count line 38

Source documentation

The empty case costs nothing; the only nonempty case is one of the already-bounded conductor families above the threshold.

theorem page_kernel_exclusion_count (P : PublishedProgressionInput) (Q : ℕ) (R E : ℝ)
    (S T : Finset ℤ) (f g : ℤ → ℤ) (hE : 0 ≤ E)
    (hcount : ∀ q : ℕ, R < (q : ℝ) →
      (((S.product T).filter fun z => f z.1 * g z.2 ∈ largeConductorKernelCandidates q).card : ℝ) ≤ E) :
    (((S.product T).filter fun z => f z.1 * g z.2 ∈ pageKernelExclusion P Q R).card : ℝ) ≤ E := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.largeConductorKernelCandidates, OAI.Ostmann.pageKernelExclusion