OAI/NumberTheory/Ostmann/Arithmetic/MovingKernelSlices.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Concrete polynomial data for either slice of the two-giant kernel

  1. theorem OAI.Ostmann.movingSmoothPolynomialFactors_root_data line 11
  2. theorem OAI.Ostmann.movingRealKernel_slice_polynomial line 41
  3. theorem OAI.Ostmann.movingRealKernel_slice_root_data line 62

    Source documentation

    The root count is uniform in both real coordinate values and all fixed small primes. This is the certificate used by the joint giant comparison.

    theorem movingRealKernel_slice_root_data {σ : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (ψ : 𝓢(ℝ, ℂ))
    (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D) (hφ : ∀ x, |φ x| ≤ B)
    (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|) (coord : Bool) (fixed : ℝ) :
    let nodes := T.formulaNodes value hvalue childBound pivotBound hf (.prime false) (.prime true)
…

    Mentions: OAI.Ostmann.MovingSlotData