OAI/NumberTheory/Ostmann/Tree/PairPopulationFibers.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.filteredPairFiberEquiv line 18
2. theorem OAI.Ostmann.filteredPair_card line 32
3. theorem OAI.Ostmann.filteredPair_card_le line 43
4. theorem OAI.Ostmann.exists_large_pair_fiber line 63

   Source documentation

   If the total pair count exceeds the label count times K, a compatible pair of labels has population product greater than K.

   theorem exists_large_pair_fiber {A B C D : Type*}
       [Fintype A] [Fintype B] [Fintype C] [Fintype D]
       (f : A → C) (g : B → D) (R : C → D → Prop) (K : ℝ) (hK : 0 ≤ K)
       (hlarge : (Fintype.card {z : C × D // R z.1 z.2} : ℝ) * K <
         (Fintype.card {z : A × B // R (f z.1) (g z.2)} : ℝ)) :
       ∃ q : {z : C × D // R z.1 z.2}, K <
         (Fintype.card {x : A // f x = q.1.1} : ℝ) * Fintype.card {y : B // g y = q.1.2} := by
   …

5. def OAI.Ostmann.finsetFiberEquiv line 74
6. theorem OAI.Ostmann.finset_fiber_card line 81