OAI/Combinatorics/Progressions/Geometry/QuantitativeProjectedChart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_normalized_projected_chart line 13
  2. theorem OAI.Erdos3.projectedAxisNormBudget_le_exp line 58
  3. theorem OAI.Erdos3.projectedAxisDefectBudget_le_exp line 72
  4. theorem OAI.Erdos3.projectedAxisNormBudget_add_one_le_exp line 84
  5. theorem OAI.Erdos3.projectedChart_forwardBudget_le_exp line 92
  6. theorem OAI.Erdos3.projectedChart_inverseBudget_le_exp line 121
  7. theorem OAI.Erdos3.projectedChart_volumeBudget_le_exp line 138
  8. theorem OAI.Erdos3.projectedChart_defectBudget_le_exp line 154
  9. theorem OAI.Erdos3.exists_quantitative_projected_chart line 173