OAI/Combinatorics/Progressions/Sampling/ForecastLawNativeRawJointMean.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalDeckSource line 44
2. def OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalChartSource line 58
3. def OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget line 75
4. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_integer_deck line 84
5. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalDeckSource_cutoff line 127
6. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_cutoff line 156
7. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_cutoff_of_active_support line 190
8. theorem OAI.Erdos3.VectorPolynomial.forecast_density_physical_atom_reassociate line 262

   Also declared: OAI/Combinatorics/Progressions/Sampling/ForecastDensityPhysicalApproximation.lean:649 (same declaration text).

9. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalApproximation line 265
10. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalChartSource_normalized_raw_point line 346
11. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalChartSource_measurable line 437
12. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalChartSource_continuous line 482
13. theorem OAI.Erdos3.VectorPolynomial.exists_forecastLawDensity_native_expansion line 572
14. theorem OAI.Erdos3.VectorPolynomial.zmodReduction_val line 668

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

15. theorem OAI.Erdos3.VectorPolynomial.forecastLawNativeJointRawIntegrand line 704
16. theorem OAI.Erdos3.VectorPolynomial.forecastLawNativeJointSum line 821
17. theorem OAI.Erdos3.VectorPolynomial.forecastLawNativeRawSum_eq_jointMean line 873