OAI/Combinatorics/Progressions/Estimates/PairedDiagonalApproximation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialTopSymbolMultilinear line 12
  2. theorem OAI.Erdos3.polynomialTopSymbolMultilinear_apply line 18
  3. theorem OAI.Erdos3.polynomialTopSymbol_update_add line 24
  4. theorem OAI.Erdos3.polynomialTopSymbol_update_smul line 33
  5. def OAI.Erdos3.rowDirectionLinear line 49
  6. theorem OAI.Erdos3.rowDirectionLinear_apply line 53
  7. def OAI.Erdos3.rowTopSymbolMultilinear line 56
  8. theorem OAI.Erdos3.rowTopSymbolMultilinear_apply line 61
  9. theorem OAI.Erdos3.paired_multilinear_common_approximation line 81
  10. theorem OAI.Erdos3.row_top_common_approximation line 113
  11. theorem OAI.Erdos3.tensorDenominatorBound_le line 137
  12. theorem OAI.Erdos3.tensorDiagonalPolynomial_coeff_bound line 160
  13. theorem OAI.Erdos3.tensorDiagonalPolynomial_rational_split line 192
  14. theorem OAI.Erdos3.tensorDiagonalPolynomial_approximation line 203
  15. theorem OAI.Erdos3.integerPolynomialQuotient_coeff line 215
  16. theorem OAI.Erdos3.tensor_product_scale_le line 233
  17. theorem OAI.Erdos3.tensor_entry_bound_rescale line 242
  18. theorem OAI.Erdos3.paired_multilinear_polynomial_approximation line 268