OAI/NumberTheory/Ostmann/Quadratic/KernelPairSelection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.kernel_pair_filter_card line 13

   Source documentation

   The finite-set count and the subtype count use exactly the same pairs.

   theorem kernel_pair_filter_card (S T : Finset ℤ) (f g : ℤ → ℤ) (d : ℤ) :
       ((S.product T).filter fun z => f z.1 * g z.2 = d).card =
         Fintype.card {z : S × T // f z.1 * g z.2 = d} := by
   …

2. theorem OAI.Ostmann.kernel_pair_population_sum line 27
3. theorem OAI.Ostmann.exists_populated_nonexceptional_kernels line 58

   Source documentation

   After deleting at most E pairs belonging to one signed product, one of the other kernel pairs has a large population product.

   theorem exists_populated_nonexceptional_kernels (S T : Finset ℤ) (f g : ℤ → ℤ)
       (d : ℤ) (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
   …