OAI/NumberTheory/PowerFree/IntegralKernels.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.integralKernelMatrix line 12
  2. theorem OAI.QuarticPowerFree.mul_integralKernelMatrix line 16
  3. theorem OAI.QuarticPowerFree.integralKernelMatrix_mulVec_of_kernel line 24
  4. theorem OAI.QuarticPowerFree.gram_det_ne_zero_of_linearIndependent line 32
  5. theorem OAI.QuarticPowerFree.mulVec_eq_zero_of_row_mem_span line 50
  6. theorem OAI.QuarticPowerFree.integralKernelMatrix_column_mem_kernel line 64
  7. theorem OAI.QuarticPowerFree.mem_span_integralKernelMatrix_columns line 75
  8. theorem OAI.QuarticPowerFree.exists_independent_spanning_rows line 96
  9. theorem OAI.QuarticPowerFree.integralKernelMatrix_map line 118
  10. theorem OAI.QuarticPowerFree.det_abs_le_row_product line 136
  11. theorem OAI.QuarticPowerFree.det_abs_le_uniform line 158
  12. theorem OAI.QuarticPowerFree.matrix_mul_entry_abs_le line 165
  13. def OAI.QuarticPowerFree.integralKernelHeight line 181
  14. theorem OAI.QuarticPowerFree.integralKernelMatrix_abs_le line 185
  15. theorem OAI.QuarticPowerFree.exists_bounded_integral_kernel_spanning line 251
  16. def OAI.QuarticPowerFree.monomialOrder line 306
  17. def OAI.QuarticPowerFree.monomialsUpTo line 308
  18. theorem OAI.QuarticPowerFree.mem_monomialsUpTo line 312
  19. theorem OAI.QuarticPowerFree.card_monomialsUpTo line 320
  20. def OAI.QuarticPowerFree.polynomialFromCoefficients line 333
  21. theorem OAI.QuarticPowerFree.polynomialFromCoefficients_coeff line 343
  22. theorem OAI.QuarticPowerFree.polynomialFromCoefficients_coeff_of_not_mem line 352
  23. theorem OAI.QuarticPowerFree.polynomialFromCoefficients_support line 364
  24. theorem OAI.QuarticPowerFree.polynomialFromCoefficients_coefficients line 372
  25. theorem OAI.QuarticPowerFree.polynomialFromCoefficients_map line 384
  26. theorem OAI.QuarticPowerFree.eval_polynomialFromCoefficients line 391
  27. theorem OAI.QuarticPowerFree.polynomialFromCoefficients_totalDegree line 398
  28. theorem OAI.QuarticPowerFree.exists_bounded_polynomial_kernel line 405
  29. theorem OAI.QuarticPowerFree.monomial_eval_abs_le line 459
  30. theorem OAI.QuarticPowerFree.exists_bounded_degree_vanishing_polynomials line 474