OAI/NumberTheory/Ostmann/Tree/BadPartitionCounts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.BadPartitionPair line 13
2. abbrev OAI.Ostmann.BadPartitionWitness line 19
3. abbrev OAI.Ostmann.BadPartitionWitness.Matching line 21
4. theorem OAI.Ostmann.card_badPartitionPair_le line 25
5. theorem OAI.Ostmann.card_badPartitionWitness_le line 32
6. def OAI.Ostmann.badPartitionCost line 43
7. theorem OAI.Ostmann.badPartitionCost_nonneg line 46
8. theorem OAI.Ostmann.badPartition_matching_bound line 50
9. theorem OAI.Ostmann.badPartition_total_bound line 87

   Source documentation

   Sum over every possible pair of component partitions. The prefactor depends only on r, and not on the number m of slots at a leaf.

   theorem badPartition_total_bound {r : ℕ} (hr : 1 ≤ r) (m : ℕ) :
       (Fintype.card (Σ w : BadPartitionWitness r, w.Matching m) : ℝ) ≤
         ((r + 1) * r ^ (2 * r) : ℕ) * badPartitionCost r m := by
   …

   Mentions: OAI.Ostmann.BadPartitionWitness, OAI.Ostmann.badPartitionCost