OAI/Combinatorics/Progressions/Linear/KernelSupportContraction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.productKernelApply line 15
  2. theorem OAI.Erdos3.productKernelApply_eq_matrix line 19
  3. theorem OAI.Erdos3.productKernelApply_conditional line 23
  4. theorem OAI.Erdos3.productKernelApply_sum line 30
  5. theorem OAI.Erdos3.productKernelApply_smul line 35
  6. def OAI.Erdos3.anovaKernelMatrix line 53
  7. theorem OAI.Erdos3.productKernelApply_ANOVA line 58
  8. theorem OAI.Erdos3.productKernelApply_ANOVA_active line 91
  9. theorem OAI.Erdos3.anovaKernelMatrix_sq_le line 120
  10. theorem OAI.Erdos3.productKernelApply_ANOVA_sq_le line 140
  11. theorem OAI.Erdos3.productCouplingPairing_support_sq_le line 146