OAI/NumberTheory/Ostmann/Arithmetic/JointLineComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.sampledPrimeLineProbability line 13
2. theorem OAI.Ostmann.sampledPrimeLineProbability_eq_flags line 22
3. theorem OAI.Ostmann.joint_line_flag_comparison_le line 43
4. theorem OAI.Ostmann.joint_line_probability_comparison_le line 88

   Source documentation

   All local integrals can be replaced together even when their coefficient polynomials depend on the other sampled internal primes.

   theorem joint_line_probability_comparison_le {A I : Type*} [Fintype A] [Nonempty A] [Fintype I]
       (J : I → Type*) [∀ b, Fintype (J b)] {n : ℕ}
       (value : A → ℤ) (hinj : Function.Injective value)
       (prime : A → ℕ) (hpInj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
       (L : ∀ b, J b → PolynomialGiantLine (Fin (n + 1))) (i : ∀ b, J b)
       (coordinate : I → Fin (n + 1)) (external : Bool)
       (habsent : ∀ b s, coordinate b ∉ (lineTestPolynomials (L b) (i b) s).vars)
       (μ : Fin (n + 1) → A → ℝ) (hμ : ∀ j a, 0 ≤ μ j a)
       (hmass : ∀ j, ∑ a, μ j a = 1)
       (α β V H : ℝ) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hV : 0 < V) (hH : 1 ≤ H)
       (hmax : ∀ j a, μ j a ≤ α) (hpmax : ∀ b a, μ (coordinate b) a ≤ β)
       (hsize : ∀ a, V ≤ Real.log (prime a : ℝ))
   …

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