OAI/NumberTheory/Ostmann/Construction/DyadicSupportedHistory.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.boundedDyadicIndex line 13
2. theorem OAI.Ostmann.boundedDyadicIndex_eq line 16
3. theorem OAI.Ostmann.dyadic_progression_padding line 20
4. theorem OAI.Ostmann.dyadic_supported_history_bound line 33

   Source documentation

   Every sharp support condition is retained. The loss for all long-prime dyadic pieces is only their count, and the original normalizing mass remains.

   theorem dyadic_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 E M : ℕ) [NeZero M] (hA : 0 < A) (hMA : M ≤ A)
       (hM : ∀ q : Q, M.Coprime (q : ℕ))
       (hlow : ∀ p ∈ P, 2 * A ≤ p) (hhigh : ∀ p ∈ P, p ≤ E)
       (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 : ℕ)
   …

   Mentions: OAI.Ostmann.ClippedPolynomialFactor