OAI/Combinatorics/Progressions/Linear/KernelCoreComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.prod_support_factor_bound line 17
  2. theorem OAI.Erdos3.productCouplingPairing_level_abs_le line 34
  3. theorem OAI.Erdos3.productCouplingPairing_tail_abs_le line 46
  4. theorem OAI.Erdos3.productCouplingPairing_level_of_bounds line 58
  5. theorem OAI.Erdos3.productCouplingPairing_low_levels_small line 79
  6. theorem OAI.Erdos3.finiteKernel_contraction_sq line 119
  7. theorem OAI.Erdos3.productCouplingPairing_restricted_tail_abs_le line 126
  8. theorem OAI.Erdos3.productKernel_conditioning_shell_bound line 159
  9. theorem OAI.Erdos3.productKernel_conditioning_shell_of_truncated line 195
  10. theorem OAI.Erdos3.productCouplingPairing_restricted_level_of_bounds line 247
  11. theorem OAI.Erdos3.productCouplingPairing_restricted_low_levels_small line 265
  12. theorem OAI.Erdos3.productKernel_core_comparison line 299