OAI/Combinatorics/SumProduct/Alignment/BoxPolynomial01.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoxPolynomialLines.boxMean line 16
  2. theorem OAI.BoxPolynomialLines.boxMean_zero line 20
  3. theorem OAI.BoxPolynomialLines.boxMean_succ line 22
  4. theorem OAI.BoxPolynomialLines.boxMean_sub line 25
  5. theorem OAI.BoxPolynomialLines.boxMean_const line 31
  6. theorem OAI.BoxPolynomialLines.boxMean_comm line 37
  7. theorem OAI.BoxPolynomialLines.boxMean_norm_le line 47
  8. theorem OAI.BoxPolynomialLines.exists_norm_ge line 63
  9. theorem OAI.BoxPolynomialLines.cons_add line 77
  10. theorem OAI.BoxPolynomialLines.norm_mean_sub_le line 84
  11. theorem OAI.BoxPolynomialLines.tail_shift_bound line 91
  12. theorem OAI.BoxPolynomialLines.shift_step line 104
  13. theorem OAI.BoxPolynomialLines.norm_shift_error line 132
  14. theorem OAI.BoxPolynomialLines.mean_const line 143
  15. theorem OAI.BoxPolynomialLines.line_average_error line 146
  16. theorem OAI.BoxPolynomialLines.exists_correlated_line line 159
  17. theorem OAI.BoxCounting.mean_eq_fin line 185
  18. theorem OAI.BoxCounting.boxMean_eq_fin line 195
  19. def OAI.BoxCounting.indicator line 218
  20. def OAI.BoxCounting.count line 222
  21. theorem OAI.BoxCounting.boxMean_indicator line 228
  22. def OAI.DenseBoxModularPolynomial.eval line 246
  23. theorem OAI.DenseBoxModularPolynomial.circleNorm_le_integer_error line 249
  24. theorem OAI.DenseBoxModularPolynomial.circleNorm_le_one line 253
  25. theorem OAI.DenseBoxModularPolynomial.division_length line 257
  26. theorem OAI.DenseBoxModularPolynomial.common_denominator line 265
  27. theorem OAI.DenseBoxModularPolynomial.line_scale_coeff line 289
  28. def OAI.DenseBoxModularPolynomial.indicator line 293
  29. lemma OAI.DenseBoxModularPolynomial.norm_indicator line 297
  30. lemma OAI.DenseBoxModularPolynomial.mean_indicator line 302
  31. lemma OAI.DenseBoxModularPolynomial.abs_multiplier line 312
  32. theorem OAI.DenseBoxModularPolynomial.line_test_constants line 322
  33. theorem OAI.DenseBoxModularPolynomial.lattice_inverse line 398
  34. theorem OAI.DenseBoxModularPolynomial.lattice_inverse_cardinal line 437