OAI/Combinatorics/Progressions/Estimates/AllocatedCoveredFixedTest.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finitePMF_integral_measurable line 15
  2. theorem OAI.Erdos3.finitePMF_integral_norm_le line 22
  3. theorem OAI.Erdos3.finitePMF_integral_comp line 28
  4. theorem OAI.Erdos3.probabilityProduct_finiteMean line 37
  5. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetDensity_integral line 68
  6. def OAI.Erdos3.VectorPolynomial.allocatedMixedJetReconstruct line 110
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedJetReconstruct_measurable line 115
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedJetReconstruct_physical line 121
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedJetReconstruct_physical_split line 141
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_frozen_supported line 151
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalMixedJet_test_mean line 195
  12. def OAI.Erdos3.VectorPolynomial.allocatedDeckMixedTest line 273
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedDeckMixedTest_measurable line 278
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedDeckMixedTest_norm_le line 285
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalMixedDeck_test_mean line 296
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredPullback_measurable line 388
  17. def OAI.Erdos3.VectorPolynomial.allocatedCoveredFixedTest line 394
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredFixedTest_measurable line 400
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredFixedTest_norm_le line 408
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCovered_test_mean line 418