OAI/Combinatorics/Progressions/Estimates/AllocatedCoveredSiteExpansion.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJet_restrictedDensity_eq line 31
  2. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJet_restrictedDensity_measurable line 47
  3. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJet_restrictedComplexDensity_eq line 82
  4. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJet_restrictedComplexDensity_measurable line 102
  5. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJet_normalized_complex_integral line 144
  6. theorem OAI.Erdos3.restrictedComplexChartDensity_weighted_integral_of_map line 189
  7. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJet_reference_map line 243
  8. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJet_weighted_complex_integral line 257
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity_measurable line 322
  10. def OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity line 344
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_sub line 356
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_measurable line 366
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_lintegral_abs line 387
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_integrable line 443
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_integral_abs line 453
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_l1 line 465
  17. def OAI.Erdos3.VectorPolynomial.allocatedCoveredComplexProfileDensity line 515
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredComplexProfileDensity_real line 524
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredComplexProfileDensity_sum line 535
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredComplexProfileDensity_pointwise_error line 556
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_abs_mono line 614
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_zero line 672
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredProfileDensity_abs line 682
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredComplexProfileDensity_pointwise_abs_error line 694
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredSiteTermDensity_error line 747
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredIdealSiteApproximation_error line 774