OAI/NumberTheory/Ostmann/Characters/FiniteKernelExclusion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.kernel_pair_filter_mem_card line 11
2. theorem OAI.Ostmann.kernel_pair_finite_exclusion_bound line 27
3. theorem OAI.Ostmann.exists_populated_outside_kernel_family line 36

   Source documentation

   The surviving kernel pair carries a large product of the actual endpoint populations, after deletion of every product in D.

   theorem exists_populated_outside_kernel_family (S T : Finset ℤ) (f g : ℤ → ℤ)
       (D : Finset ℤ) (E K : ℝ) (hK : 0 ≤ K)
       (hbad : (((S.product T).filter fun z => f z.1 * g z.2 ∈ D).card : ℝ) ≤ E)
       (hlarge : ((S.image f).card : ℝ) * (T.image g).card * K + E <
         (S.card : ℝ) * T.card) :
       ∃ u ∈ S.image f, ∃ v ∈ T.image g, u * v ∉ D ∧
         K < ((S.filter fun x => f x = u).card : ℝ) * (T.filter fun y => g y = v).card := by
   …