KernelPopulationRetention.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative retention of small, populated kernel fibers

theorem OAI.Ostmann.eventual_small_kernel_fibers_decay line 14

theorem OAI.Ostmann.eventual_populated_kernel_retention line 53

Source documentation

At least half the original population remains in entire fibers whose kernels are small and whose individual sizes reach the split-prime cutoff.

theorem eventual_populated_kernel_retention (η ε a : ℝ)
    (hη : 0 < η) (hηU : η ≤ 1 / 1000) (hε : 0 ≤ ε) (hεη : ε ≤ η / 100)
    (ha : 0 < a) :
    ∀ᶠ L : ℝ in atTop, ∀ (S : Finset ℤ) (f : ℤ → ℤ) (root : ℤ → ℕ)
      (m : ℕ) (h : ℤ),
      0 < m → (m : ℝ) ≤ Real.exp (η * L) → h.natAbs.Coprime m →
      ((S.image f).card : ℝ) ≤ Real.exp (3 * ε * L) →
      (∀ x ∈ S, f x * (root x : ℤ) ^ 2 = (m : ℤ) * x - h) →
      (∀ x ∈ S, ∀ y ∈ S, |((x - y : ℤ) : ℝ)| ≤ Real.exp L) →
      a * Real.exp (L / 2) / L ^ 6 ≤ S.card →
      (a / 2) * Real.exp (L / 2) / L ^ 6 ≤
        (populatedKernelPoints S f (fun u => |(u : ℝ)| ≤ Real.exp (η * L))
…

Mentions: OAI.Ostmann.populatedKernelPoints