OAI/Combinatorics/Progressions/Estimates/NormalizedJetColumns.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.frozenTupleCoordinate line 11
  2. theorem OAI.Erdos3.frozenTupleCoordinate_eval line 15
  3. theorem OAI.Erdos3.frozenTupleCoordinate_mass_le line 19
  4. theorem OAI.Erdos3.frozenTupleCoordinate_degree_le line 25
  5. def OAI.Erdos3.normalizedJetColumn line 29
  6. theorem OAI.Erdos3.normalizedJetColumn_degree_le line 33
  7. theorem OAI.Erdos3.normalizedJetColumn_mass_le line 39
  8. theorem OAI.Erdos3.normalizedJetColumns_apply_coefficients line 50
  9. def OAI.Erdos3.normalizedJetMass line 60
  10. theorem OAI.Erdos3.normalizedJetColumns_lipschitzOn_box line 63