OAI/Combinatorics/Progressions/Linear/MixedPairPartitionKernel.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.norm_unit_prod_sub_prod_le_sum line 13
  2. theorem OAI.Erdos3.norm_cubic_pair_product_sub_le line 41
  3. def OAI.Erdos3.NativeCubicPairPartition.cellWeight line 86
  4. theorem OAI.Erdos3.NativeCubicPairPartition.cellWeight_nonneg line 89
  5. theorem OAI.Erdos3.NativeCubicPairPartition.cellWeight_total line 92
  6. def OAI.Erdos3.NativeCubicPairPartition.cellVector line 95
  7. theorem OAI.Erdos3.NativeCubicPairPartition.cellVector_norm line 99
  8. def OAI.Erdos3.NativeCubicPairPartition.cellKernel line 103
  9. theorem OAI.Erdos3.NativeCubicPairPartition.weighted_kernel_error line 107
  10. theorem OAI.Erdos3.NativeCubicPairPartition.kernel_approximation line 137
  11. theorem OAI.Erdos3.NativeCubicPairPartition.exists_correlating_cell line 146
  12. theorem OAI.Erdos3.norm_unit_pair_products_sub_le line 167
  13. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticTensorIndex line 206
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticTensor_eval line 209
  15. def OAI.Erdos3.NativeQuarticPairPartition.cellWeight line 231
  16. theorem OAI.Erdos3.NativeQuarticPairPartition.cellWeight_nonneg line 234
  17. theorem OAI.Erdos3.NativeQuarticPairPartition.cellWeight_total line 237
  18. def OAI.Erdos3.NativeQuarticPairPartition.cellVector line 240
  19. theorem OAI.Erdos3.NativeQuarticPairPartition.cellVector_norm line 244
  20. def OAI.Erdos3.NativeQuarticPairPartition.cellKernel line 248
  21. theorem OAI.Erdos3.NativeQuarticPairPartition.weighted_kernel_error line 252
  22. theorem OAI.Erdos3.NativeQuarticPairPartition.kernel_approximation line 294
  23. theorem OAI.Erdos3.NativeQuarticPairPartition.exists_correlating_cell line 303
  24. def OAI.Erdos3.NativeMixedPairPartition.cellWeight line 348
  25. theorem OAI.Erdos3.NativeMixedPairPartition.cellWeight_nonneg line 351
  26. theorem OAI.Erdos3.NativeMixedPairPartition.cellWeight_total line 354
  27. def OAI.Erdos3.NativeMixedPairPartition.cellVector line 357
  28. theorem OAI.Erdos3.NativeMixedPairPartition.cellVector_norm line 361
  29. def OAI.Erdos3.NativeMixedPairPartition.cellKernel line 365
  30. theorem OAI.Erdos3.NativeMixedPairPartition.weighted_kernel_error line 369
  31. theorem OAI.Erdos3.NativeMixedPairPartition.kernel_approximation line 410
  32. theorem OAI.Erdos3.NativeMixedPairPartition.exists_correlating_cell line 419