OAI/Combinatorics/Progressions/Sampling/ForecastInactiveFixedSupport.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_bounded_grid_site_expansion line 19
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerCoefficient_scaled_bound line 134
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerJet_scaled_support_bound line 159
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity_scaled_support_bound line 179
  5. def OAI.Erdos3.VectorPolynomial.allocatedWholeGridJetPMF line 220
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeGridJetPMF_toReal line 231
  7. instance OAI.Erdos3.VectorPolynomial.allocatedGridJetRow_countable line 247
  8. instance OAI.Erdos3.VectorPolynomial.allocatedGridJetRow_measurableSingleton line 254
  9. def OAI.Erdos3.VectorPolynomial.allocatedSupportedGridJetPMF line 261
  10. def OAI.Erdos3.VectorPolynomial.allocatedSupportedGridJetDensity line 273
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeGridJetPMF_joint_law line 281
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity_conditional_mean line 313
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridPMF_base_independent line 362
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridPMF_scaled_support line 371
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_bounded_grid_site_expansion line 398
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedGridSide_normalizable_or_bounded line 441
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedGridJetPMF_scaled_support_bound line 489
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridPMF_natural_support line 554
  19. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_natural_bounded_grid_site_expansion line 575
  20. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_fixed_mem_physical_support line 653
  21. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_fixed_natural_support line 666
  22. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_fixed_bounded_site_expansion line 678