OAI/Combinatorics/Progressions/Sampling/AllocatedOriginalSampleForecastMeanRiemann.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource line 47
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource_ae_density line 56
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource_density_of_supported line 118
  4. def OAI.Erdos3.canonicalZeroSpatialLaw line 147
  5. theorem OAI.Erdos3.canonicalZeroSpatialLaw_eq_density line 155
  6. theorem OAI.Erdos3.canonicalZeroSpatialLaw_probability line 165
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_fixed_measurable line 198
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource_probability line 208
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource_integral line 219
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource_real_integral line 232
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastPartial_measurable line 245
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastPartial_norm_le line 254
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastPartial_integrable line 263
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastSource_progression_density line 304
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastExpectation_eq_iterated line 372
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastExpectation_norm_le line 384
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFiniteExpectation_measurable line 396
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFiniteExpectation_norm_le line 409
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastExpectation_measurable line 422
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecast_contained_residue_riemann line 467
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecast_contained_residue_complex_riemann line 550
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecast_contained_residue_ae_complex_riemann line 685
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecast_contained_residue_mean_complex_riemann line 753