OAI/Combinatorics/Progressions/Sampling/ForecastDensityPhysicalApproximation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.forecast_single_cutoff_error line 11
  2. theorem OAI.Erdos3.forecast_buffered_chart_twist_expansion line 23
  3. theorem OAI.Erdos3.forecast_buffered_twist_coefficient_mass line 53
  4. theorem OAI.Erdos3.forecastPhysicalBufferedError line 74
  5. theorem OAI.Erdos3.forecastPhysicalBufferedCoefficientMass line 110
  6. theorem OAI.Erdos3.VectorPolynomial.exists_forecastDensityBufferedTwist line 148
  7. theorem OAI.Erdos3.VectorPolynomial.exists_forecastDensityBufferedPhysicalAtom line 287
  8. def OAI.Erdos3.VectorPolynomial.forecastDensityNormalizedAtom line 432
  9. theorem OAI.Erdos3.VectorPolynomial.exists_forecastDensityBufferedNativeExpansion line 455
  10. theorem OAI.Erdos3.VectorPolynomial.forecast_density_physical_atom_reassociate line 649

    Also declared: OAI/Combinatorics/Progressions/Sampling/ForecastLawNativeRawJointMean.lean:262 (same declaration text).

  11. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalApproximation line 652