OAI/Combinatorics/Progressions/Sampling/ForecastLawPhysicalAmbientHaarComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.nativeFiniteExpansion_mean_comparison line 13
  2. theorem OAI.Erdos3.VectorPolynomial.exists_nativeForecast_ambient_comparison line 55
  3. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_nativeHaarExpansion line 168
  4. def OAI.Erdos3.VectorPolynomial.nativeForecastAmbientExponent line 259
  5. theorem OAI.Erdos3.VectorPolynomial.nativeForecastAmbientExponent_ge_two line 262
  6. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_ambientHaarComparison line 268
  7. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_nativeHaarExpansion line 405
  8. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_ambientHaarComparison line 498