OAI/NumberTheory/Ostmann/Quadratic/CommonCenterConcreteMoments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.intervalMatchingLiftEquiv line 11
2. theorem OAI.Ostmann.interval_factorial_moment_le line 24

   Source documentation

   The lower-order moment upper bound follows from counting residue-class lifts of each ordered distinct prime tuple.

   theorem interval_factorial_moment_le (P : Finset ℕ) (hprime : ∀ p ∈ P, p.Prime)
       (a : ℤ) (t : ℕ → ℤ) (r H Z : ℕ) (hZ : 0 < Z) (hmin : ∀ p ∈ P, Z ≤ p) :
       (∑ n : (Finset.Ico (-(H : ℤ)) (H + 1)),
         ((matchingPrimes P a t n.1).card.descFactorial r : ℝ)) ≤
       (P.card.descFactorial r : ℝ) * ((2 * (H : ℝ) + 1) / (Z : ℝ) ^ r + 1) := by
   …

   Mentions: OAI.Ostmann.matchingPrimes

3. theorem OAI.Ostmann.interval_factorial_moment_ge line 51

   Source documentation

   A supplied family of witnessed tuples gives the high moment directly.

   theorem interval_factorial_moment_ge (P : Finset ℕ) (a : ℤ) (t : ℕ → ℤ) (r H : ℕ)
       (E : Finset (Fin r ↪ P))
       (hlift : ∀ e ∈ E, ∃ n ∈ Finset.Ico (-(H : ℤ)) (H + 1),
         ∀ i, ((e i).1 : ℤ) ∣ n - a * t (e i).1) :
       (E.card : ℝ) ≤ ∑ n : (Finset.Ico (-(H : ℤ)) (H + 1)),
         ((matchingPrimes P a t n.1).card.descFactorial r : ℝ) := by
   …

   Mentions: OAI.Ostmann.matchingPrimes

4. theorem OAI.Ostmann.liftInterval_log_difference line 67

   Source documentation

   The interval length supplies the prime-intersection logarithmic budget.

   theorem liftInterval_log_difference (H K : ℕ) (V : ℝ)
       (hbudget : Real.log (2 * (H : ℝ)) < (K + 1 : ℕ) * V)
       (n m : ℤ) (hn : n ∈ Finset.Ico (-(H : ℤ)) (H + 1))
       (hm : m ∈ Finset.Ico (-(H : ℤ)) (H + 1)) (hne : n ≠ m) :
       Real.log ((n - m).natAbs : ℝ) < (K + 1 : ℕ) * V := by
   …