OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticIntegerComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.integerTestValue line 12
2. theorem OAI.Ostmann.integer_polynomial_symbolic_comparison_le line 18

   Source documentation

   The signed replacement estimate with all zero and divisor-count bridges proved for the actual integer polynomial evaluations.

   theorem integer_polynomial_symbolic_comparison_le {A I : Type*} [Fintype A] [Fintype I]
       {n : ℕ} (value : A → ℤ) (hinj : Function.Injective value)
       (F : I → MvPolynomial (Fin n) ℤ)
       (μ : Fin n → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
       (hmass : ∀ i, ∑ a, μ i a = 1)
       (α : ℝ) (hα : 0 ≤ α) (hmax : ∀ i a, μ i a ≤ α)
       (P : Finset ℕ) (hprime : ∀ p ∈ P, p.Prime)
       (ν : ℕ → ℝ) (hν : ∀ p ∈ P, 0 ≤ ν p) (hνmass : ∑ p ∈ P, ν p = 1)
       (β V H : ℝ) (hβ : 0 ≤ β) (hV : 0 < V) (hH : 1 ≤ H)
       (hνmax : ∀ p ∈ P, ν p ≤ β) (hsize : ∀ p ∈ P, V ≤ Real.log (p : ℝ))
       (hvalue : ∀ i x, |(integerTestValue value (F i) x : ℝ)| ≤ H)
       (Ψ : (Fin n → A) → ℕ → (I → Bool) → ℂ)
   …

   Mentions: OAI.Ostmann.integerTestValue