OAI/Combinatorics/Progressions/Probability/AllocatedProbabilityWindowMesh.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedComplexGridMultiplier_real_div line 58
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor_eq_weight line 78
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor_norm line 92
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor_mass line 107
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedGlobalWindowPrefactor_integral_mass line 207
  6. def OAI.Erdos3.VectorPolynomial.allocatedIdealSupportCost line 246
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealSupportCost_bound line 248
  8. def OAI.Erdos3.VectorPolynomial.allocatedIdealWindowMassLog line 259
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealWindowMassLog_nonneg line 265
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealWindowMassLog_mono line 274
  11. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedIdealWindowMassLog_bound line 294
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal_zero_outside line 323
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealGlobalWindow_mass line 357
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongIdeal_reference_mass line 422
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealGlobalWindow_probability_mass line 510
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealProbability_mesh_of_scale line 552
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteScale_probability_mesh line 575