OAI/Combinatorics/Progressions/Dynamics/AllocatedFiniteIdealMaskBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedFiniteIdealProfileLog line 13
  2. def OAI.Erdos3.VectorPolynomial.allocatedFiniteIdealCoefficientLog line 16
  3. def OAI.Erdos3.VectorPolynomial.allocatedFiniteIdealLipschitzLog line 21
  4. theorem OAI.Erdos3.VectorPolynomial.idealSiteLogBudget_le_finite_profile line 24
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteIdeal_budget_nonneg line 32
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteIdeal_coefficient_log_le line 41
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteIdeal_coefficient_budget line 83
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteIdeal_buffered_lipschitz_budget line 95
  9. def OAI.Erdos3.VectorPolynomial.allocatedFiniteIdealMaskedLog line 157
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteIdeal_mask_cost line 162
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedFiniteIdeal_masked_coefficient_budget line 228