OAI/Combinatorics/Progressions/Sampling/ForecastActualPhysicalSourceContinuous.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedShortIntegerSelection_exhaustive line 18
  2. theorem OAI.Erdos3.VectorPolynomial.forecastBufferedPhysicalChartCutoff_eq line 60
  3. theorem OAI.Erdos3.VectorPolynomial.forecastBufferedPhysicalChartCutoff_eq_one line 76
  4. theorem OAI.Erdos3.VectorPolynomial.forecastBufferedPhysicalChartCutoff_eq_one_of_box line 86
  5. theorem OAI.Erdos3.integerMatrix_mulVec_scaled_bound line 105
  6. theorem OAI.Erdos3.rationalInactiveForecast_eq_zero_of_not_mem_range line 127
  7. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_scaled_bound line 150
  8. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_normalized_bound line 187
  9. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixed_rational_eq_zero_of_outside line 204
  10. theorem OAI.Erdos3.VectorPolynomial.forecastOriginalSource_coordinates_bound line 274
  11. theorem OAI.Erdos3.VectorPolynomial.forecastOriginalSource_cutoff_eq_one line 297
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSource_cutoff line 361
  13. def OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalDeckSource line 445
  14. def OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource line 459
  15. def OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget line 476
  16. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_integer_deck line 485
  17. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalDeckSource_cutoff line 528
  18. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_cutoff line 557
  19. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_cutoff_of_active_support line 591
  20. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_normalized_raw_point line 661
  21. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_measurable line 752
  22. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_weighted_haar_integral line 816
  23. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_norm_le line 890
  24. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_continuous line 954