OAI/Combinatorics/Progressions/Sampling/ForecastNativeRawSpatialFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_mem_quarter line 53
  2. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_haar_integral_unrestricted line 88
  3. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_integrable line 185
  4. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_mul_test_integrable line 215
  5. theorem OAI.Erdos3.VectorPolynomial.forecastNativeHaarMean_eq_rawSum line 301
  6. theorem OAI.Erdos3.VectorPolynomial.forecastNativeRawMean_normalization line 361
  7. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_haar_normalized_split_integral line 435
  8. def OAI.Erdos3.VectorPolynomial.forecastNativeRawSpatialFamily line 543
  9. theorem OAI.Erdos3.VectorPolynomial.allShortSelection_exhaustive line 547

    Distinct definitions of this name: OAI/Combinatorics/Progressions/Sampling/ForecastLawOriginalNativeHaarJointMean.lean:496 (same statement text; different proof or body). Qualify references as OAI.Erdos3.VectorPolynomial.allShortSelection_exhaustive@path.

  10. theorem OAI.Erdos3.VectorPolynomial.forecastNativeRawSpatialFamily_integrable line 556
  11. theorem OAI.Erdos3.VectorPolynomial.forecastNativeRawSpatialFamily_original_zero_outside line 595
  12. theorem OAI.Erdos3.VectorPolynomial.forecastNativeRawSpatialFamily_original_integrable line 609
  13. theorem OAI.Erdos3.VectorPolynomial.forecastNativeRawSpatialFamily_original_normalized_integral line 637