OAI/NumberTheory/Ostmann/Quadratic/CommonCenterMoments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.descFactorial_gap_le line 12
2. theorem OAI.Ostmann.smallCenter_factorial_moment_le line 19

   Source documentation

   Small matching sets contribute only a power of the threshold times a lower moment.

   theorem smallCenter_factorial_moment_le {I : Type*} [Fintype I]
       (r : I → ℕ) (k d : ℕ) (hd : d ≤ k) (A : ℝ) (hA : 0 ≤ A) :
       (∑ i : I, if (r i : ℝ) < A then ((r i).descFactorial k : ℝ) else 0) ≤
         A ^ d * ∑ i : I, ((r i).descFactorial (k - d) : ℝ) := by
   …

3. theorem OAI.Ostmann.highCenter_factorial_moment_ge line 36

   Source documentation

   The mass surviving the small-set removal is a moment of high matching sets.

   theorem highCenter_factorial_moment_ge {I : Type*} [Fintype I]
       (r : I → ℕ) (k d : ℕ) (hd : d ≤ k) (A B L : ℝ) (hA : 0 ≤ A)
       (hlo : (∑ i : I, ((r i).descFactorial (k - d) : ℝ)) ≤ B)
       (hhi : L ≤ ∑ i : I, ((r i).descFactorial k : ℝ)) :
       L - A ^ d * B ≤
         ∑ i : I, if A ≤ (r i : ℝ) then ((r i).descFactorial k : ℝ) else 0 := by
   …

4. theorem OAI.Ostmann.exists_commonCenter_from_factorial_moments line 58

   Source documentation

   The two factorial moment estimates in quad-lift-factorials produce a common center.

   theorem exists_commonCenter_from_factorial_moments {I P : Type*}
       [Fintype I] [Fintype P] [DecidableEq P]
       (S : I → Finset P) (k d : ℕ) (hd : d ≤ k + 1) (A K B L : ℝ)
       (hA : 0 < A) (hK : 0 ≤ K)
       (hinter : ∀ i j, i ≠ j → ((S i ∩ S j).card : ℝ) ≤ K)
       (hsmall : 2 * K * (Fintype.card P : ℝ) ≤ A ^ 2)
       (hlo : (∑ i : I, ((S i).card.descFactorial (k + 1 - d) : ℝ)) ≤ B)
       (hhi : L ≤ ∑ i : I, ((S i).card.descFactorial (k + 1) : ℝ))
       (hpositive : 0 < L - A ^ d * B) :
       ∃ i : I, A ≤ ((S i).card : ℝ) ∧
         L - A ^ d * B ≤ 2 * (Fintype.card P : ℝ) * ((S i).card : ℝ) ^ k := by
   …