OAI/Combinatorics/Progressions/Lattices/UniformDerivativeLatticeExtraction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.derivative_covolume_budget_le_exp line 10
  2. theorem OAI.Erdos3.derivative_extended_budget_le_exp line 34
  3. theorem OAI.Erdos3.derivative_output_exponent_le line 48
  4. theorem OAI.Erdos3.derivative_output_budgets_le_exp line 52
  5. theorem OAI.Erdos3.derivative_projection_budget_le_exp line 86
  6. theorem OAI.Erdos3.lattice_subspace_budgets_le_exp line 119
  7. theorem OAI.Erdos3.euclideanDerivative_lattice_extraction line 167
  8. theorem OAI.Erdos3.euclideanDerivative_uniform_lattice_extraction line 251