OAI/NumberTheory/Ostmann/Arithmetic/SupportedHistoryCancellation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.supportedHistoryAmplitude line 13
2. theorem OAI.Ostmann.supportedHistoryAmplitude_eq line 21
3. theorem OAI.Ostmann.harmonic_supported_history_bound line 33

   Source documentation

   All residue gates and sharp smooth-argument ranges are the actual tests on the sampled integers. No hypothesis asserting their regularity is needed.

   theorem harmonic_supported_history_bound {σ I : Type*} [Fintype I] {n : ℕ}
       (P Q : Finset ℕ) (hprime : ∀ q ∈ Q, q.Prime)
       (χ : ∀ q : Q, DirichletCharacter ℂ (q : ℕ)) (hnonprincipal : ∀ q, χ q ≠ 1)
       (a M K : ℕ) [NeZero M] (ha : 0 < a) (hM : ∀ q : Q, M.Coprime (q : ℕ))
       (hlow : ∀ p ∈ P, a ≤ p) (hhigh : ∀ p ∈ P, p < a + K * M)
       (b : ℝ) (hb : 0 < b) (hbQ : ∀ q ∈ Q, b ≤ (q : ℝ))
       (hPmass : 0 < ∑ p ∈ P, (p : ℝ)⁻¹) (hQmass : 0 < ∑ q ∈ Q, (q : ℝ)⁻¹)
       (N : Q → I → MvPolynomial σ ℤ) (d : Q → I → ℤ) (s : Q → I → ℕ)
       (fixed : Q → σ → ℤ) (coord : σ)
       (hd : ∀ q j, d q j ≠ 0) (hdiv : ∀ q j, d q j * s q j ∣ (M : ℤ))
       (F : Q → Fin n → ClippedPolynomialFactor) (B : ℝ) (D Bq : ℕ)
       (hB : 0 ≤ B) (hbudget : ∀ q, smoothPolynomialBudget (F q) ≤ B)
   …

   Mentions: OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.smoothPolynomialBudget