OAI/Combinatorics/Progressions/Lattices/CellResidueCorrelation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finite_fiber_mean_square line 11
  2. theorem OAI.Erdos3.finite_fiber_energy_sum line 37
  3. theorem OAI.Erdos3.finite_fiber_square_sum_le line 46
  4. theorem OAI.Erdos3.finite_residue_energy_bound line 61
  5. theorem OAI.Erdos3.finite_matching_residue_mean line 86
  6. theorem OAI.Erdos3.finite_matching_residue_energy line 107
  7. theorem OAI.Erdos3.finite_matching_kernel_error line 131
  8. theorem OAI.Erdos3.finite_matching_kernel_approximation line 166
  9. theorem OAI.Erdos3.finite_cell_residue_kernel_expand line 203
  10. theorem OAI.Erdos3.weighted_cell_residue_cancellation line 238
  11. theorem OAI.Erdos3.finite_cell_kernel_cancellation line 288
  12. theorem OAI.Erdos3.finite_cell_kernel_correlation line 307