OAI/Combinatorics/Progressions/Geometry/AllocatedSupportedSiteApproximation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.real_coordinate_support_add line 13
  2. theorem OAI.Erdos3.pmf_bind_zero_of_support line 24
  3. theorem OAI.Erdos3.pmf_integral_zero_of_support line 33
  4. theorem OAI.Erdos3.weightedModeratePlateauApproximation_zero_off_window line 42
  5. def OAI.Erdos3.VectorPolynomial.allocatedNaturalConstantRadius line 71
  6. def OAI.Erdos3.VectorPolynomial.allocatedNaturalSupportRadius line 74
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalSupportRadius_nonneg line 80
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalConstantLaw_bound line 100
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalConstantShift_bound line 124
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalPhysicalPoint_zero_off_window line 144
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalPlateau_zero_off_window line 175
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedBudgetedPlateau_zero_off_window line 188
  13. def OAI.Erdos3.VectorPolynomial.allocatedNaturalSiteRadius line 209
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalSiteRadius_nonneg line 214
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalPhysicalSites_bound line 230
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalPhysicalSites_zero_off_box line 254
  17. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_site_approximation line 308