OAI/NumberTheory/Ostmann/Quadratic/CommonCenterTupleCounts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.matchingTupleEquiv line 14

   Source documentation

   An ordered tuple of distinct primes lies in a matching set exactly when it is an embedding into that set.

   def matchingTupleEquiv {P : Type*} (S : Finset P) (r : ℕ) :
       (Fin r ↪ S) ≃ {e : Fin r ↪ P // ∀ i, e i ∈ S} where
   …

2. theorem OAI.Ostmann.card_matchingTuple line 22
3. def OAI.Ostmann.incidenceSwap line 28
4. theorem OAI.Ostmann.sum_matching_factorials line 36

   Source documentation

   Exact double counting of all ordered distinct tuple/lift incidences.

   theorem sum_matching_factorials {N P : Type*} [Fintype N] [Fintype P] [DecidableEq P]
       (S : N → Finset P) (r : ℕ) :
       (∑ n, (S n).card.descFactorial r) =
         ∑ e : Fin r ↪ P, Fintype.card {n : N // ∀ i, e i ∈ S n} := by
   …

5. theorem OAI.Ostmann.sum_matching_factorials_le line 47

   Source documentation

   A uniform bound on the number of lifts of each tuple gives the lower-order factorial-moment upper bound used by common-center extraction.

   theorem sum_matching_factorials_le {N P : Type*} [Fintype N] [Fintype P] [DecidableEq P]
       (S : N → Finset P) (r C : ℕ)
       (hcount : ∀ e : Fin r ↪ P, Fintype.card {n : N // ∀ i, e i ∈ S n} ≤ C) :
       (∑ n, (S n).card.descFactorial r) ≤ (Fintype.card P).descFactorial r * C := by
   …

6. theorem OAI.Ostmann.card_tuples_le_sum_matching_factorials line 59

   Source documentation

   A family of distinct tuples each admitting a lift supplies the high factorial-moment lower bound; no unique-lift assumption is required.

   theorem card_tuples_le_sum_matching_factorials {N P : Type*}
       [Fintype N] [Fintype P] [DecidableEq P]
       (S : N → Finset P) (r : ℕ) (E : Finset (Fin r ↪ P))
       (hlift : ∀ e ∈ E, ∃ n, ∀ i, e i ∈ S n) :
       E.card ≤ ∑ n, (S n).card.descFactorial r := by
   …