OAI/NumberTheory/Ostmann/Construction/OriginalPriorOneSidedBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.original_prior_polynomial_one_sided_bound line 14

   Source documentation

   An arbitrary original sample in the long interval is extended by zero. Its unary factor and mean are retained exactly.

   theorem original_prior_polynomial_one_sided_bound {A : Type*} [Fintype A]
       (value : A → ℕ) (hinj : Function.Injective value)
       (Q : Finset ℕ) (hprime : ∀ q ∈ Q, q.Prime)
       (χ : ∀ q : Q, DirichletCharacter ℂ (q : ℕ)) (hnonprincipal : ∀ q, χ q ≠ 1)
       (a M K : ℕ) (ha : 0 < a) (hM : ∀ q : Q, M.Coprime (q : ℕ))
       (hlow : ∀ x, a ≤ value x) (hhigh : ∀ x, value x < a + K * M)
       {n t : ℕ} (F : Q → Fin n → ClippedPolynomialFactor)
       (H : Q → Fin t → Polynomial ℝ) (keep : Q → (Fin t → Bool) → Bool)
       (B : ℝ) (R Bq : ℕ) (hB : 0 ≤ B)
       (hbudget : ∀ q, smoothPolynomialBudget (F q) ≤ B)
       (hcomplexity : ∀ q, polynomialWeightComplexity (F q) (H q) ≤ R)
       (hBq : ∀ q : Q, (q : ℕ) ≤ Bq)
   …

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