OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticLineComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.integerLineReduction line 11
2. def OAI.Ostmann.sampledLineProbability line 15
3. theorem OAI.Ostmann.sampledLineProbability_eq_flagWeight line 22
4. theorem OAI.Ostmann.integer_line_flag_comparison_le line 45

   Source documentation

   Keep the amplitude, including the spectator factors, signed while replacing the coefficient and rank flags of one internal prime.

   theorem integer_line_flag_comparison_le {A J : Type*} [Fintype A] [Fintype J]
       {n : ℕ} (value : A → ℤ) (hinj : Function.Injective value)
       (L : J → PolynomialGiantLine (Fin n)) (i : J) (external : Bool)
       (μ : Fin n → A → ℝ) (hμ : ∀ j a, 0 ≤ μ j a)
       (hmass : ∀ j, ∑ a, μ j a = 1)
       (α : ℝ) (hα : 0 ≤ α) (hmax : ∀ j a, μ j 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 : ∀ s x, |(integerTestValue value (lineTestPolynomials L i s) x : ℝ)| ≤ H)
       (F : (Fin n → A) → ℕ → ℂ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ x p, ‖F x p‖ ≤ B) :
   …

   Mentions: OAI.Ostmann.PolynomialGiantLine, OAI.Ostmann.integerTestValue, OAI.Ostmann.lineTestPolynomials

5. theorem OAI.Ostmann.sampled_line_probability_comparison_le line 81

   Source documentation

   The same estimate expressed using the actual simultaneous line counts. No rank, feasibility, or probability formula is assumed.

   theorem sampled_line_probability_comparison_le {A J : Type*} [Fintype A] [Fintype J]
       {n : ℕ} (value : A → ℤ) (hinj : Function.Injective value)
       (L : J → PolynomialGiantLine (Fin n)) (i : J) (external : Bool)
       (μ : Fin n → A → ℝ) (hμ : ∀ j a, 0 ≤ μ j a)
       (hmass : ∀ j, ∑ a, μ j a = 1)
       (α : ℝ) (hα : 0 ≤ α) (hmax : ∀ j a, μ j 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 : ∀ s x, |(integerTestValue value (lineTestPolynomials L i s) x : ℝ)| ≤ H)
       (hd : ∀ (x : Fin n → A) (p : P) j, integerLineReduction value x p (L j).denominator ≠ 0)
   …

   Mentions: OAI.Ostmann.PolynomialGiantLine, OAI.Ostmann.integerTestValue, OAI.Ostmann.lineTestPolynomials, OAI.Ostmann.integerLineReduction