MovingCanonicalComparison.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The original moving coefficient on a common residue-independent mesh

theorem OAI.Ostmann.moving_canonical_profile_bound line 29
theorem OAI.Ostmann.moving_canonical_profile_cell line 38

theorem OAI.Ostmann.PublishedProgressionInput.moving_canonical_prime_integral line 48

Source documentation

The same supplied mesh works for every admissible residue pair. Its cell multiplier is the literal residue coefficient times the real midpoint gate.

theorem PublishedProgressionInput.moving_canonical_prime_integral
    (P : PublishedProgressionInput)
    (hM : movingTopPeriod value hvalue childBound pivotBound T hf ∣ M)
    (hMq : ∀ i ∈ S, (q i : ℤ) * movingSpectatorDenominator value T ∣ (M : ℤ))
    (hR : (XR : ℤ) ≡ (b : ℤ) [ZMOD M]) (Q : ℕ)
    (hQ : 2 ≤ Q) (hq : 1 ≤ M) (hqQ : M ≤ Q) (ha : a.Coprime M)
    (roots : Finset ℝ) (s : ℕ → ℝ) (hs : Monotone s) (N : ℕ)
    (hu : 1 ≤ s 0) (hshort : s N ≤ s 0 + 1)
    (hfree : ∀ j < N, ∀ r ∈ roots, r ∉ Set.Ioo (Real.exp (s j)) (Real.exp (s (j + 1))))
    (hS : movingRealRootCuts value T nodes X lo hi false XR ⊆ roots)
    {k : ℕ} (W : Fin k → ClippedPolynomialFactor)
    (hroots : ∀ i r, r ∈ (W i).polynomial.derivative.roots → r ∈ roots) :
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.movingTopPeriod, OAI.Ostmann.movingSpectatorDenominator, OAI.Ostmann.movingRealRootCuts, OAI.Ostmann.ClippedPolynomialFactor

theorem OAI.Ostmann.moving_canonical_integer_integral line 79