OAI/Combinatorics/Progressions/Sampling/FixedSpatialKernelProgressionForecastIntegral.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastDensity line 41
  2. def OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastSource line 45
  3. def OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalForecastCap line 49
  4. def OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalForecastLip line 52
  5. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastDensity_probability_data line 71
  6. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastDensity_bounds line 85
  7. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastSource_density line 102
  8. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastSource_probability line 118
  9. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastSource_test_integral line 128
  10. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastDensity_test_integral line 139
  11. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastSource_image line 150
  12. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastDensity_image line 164
  13. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleForecastDensity_product_test_integral line 176
  14. def OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleNormalizedForecast line 190
  15. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalSampleNormalizedForecast_bounds line 194
  16. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialOriginalForecast_uniform_budget line 235
  17. def OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity line 347
  18. def OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastSource line 351
  19. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelMap_measurable line 371
  20. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelEmptyDensity_image_law line 376
  21. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastSource_density line 387
  22. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_probability_data line 410
  23. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_bounds line 425
  24. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_bounds_of_det line 443
  25. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastSource_probability line 475
  26. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_test_integral line 481
  27. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_iterated_test_integral line 520
  28. def OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalNormalizedForecast line 587
  29. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalNormalizedForecast_bounds line 601
  30. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_weighted_test_integral line 630
  31. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalNormalizedForecast_test_integral line 644
  32. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_zero_of_active_norm_gt_two line 709
  33. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_zero_of_norm_gt_two line 721
  34. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_compact line 736
  35. def OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity line 789
  36. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity_image_law line 804
  37. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity_probability_data line 815
  38. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity_bounds line 822
  39. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity_test_integral line 829
  40. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity_zero_of_active_norm_gt_two line 840
  41. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity_zero_of_norm_gt_two line 847
  42. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelSliceOriginalForecastDensity_compact line 866
  43. theorem OAI.Erdos3.fixedSpatialKernelProgression_width_pos line 886
  44. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelProgressionForecastDensity_iterated_test_integral line 948
  45. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelProgressionForecastDensity_scalarCube_iterated_test_integral line 975