OAI/Combinatorics/Progressions/Sampling/ForecastNativeJointTestBudget.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_congr_selected line 25
  2. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_congr_restrict line 58
  3. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_congr_short_restrict line 79
  4. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_join_short_restrict line 97
  5. def OAI.Erdos3.VectorPolynomial.forecastInactiveShortGrid line 138
  6. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_eq_shortGrid line 152
  7. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixedOutput_eq_shortGrid_comp line 172
  8. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSampleGrid_integer_eval line 211
  9. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSampleGrid_real_eval line 237
  10. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSampleGrid_eq_physicalMixedValue line 249
  11. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSampleShortGrid_eq_physicalMixedValue line 259
  12. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSampleShortGrid_real_eval line 277
  13. def OAI.Erdos3.VectorPolynomial.forecastShortGridSheet line 316
  14. def OAI.Erdos3.VectorPolynomial.forecastShortGridNormalized line 320
  15. theorem OAI.Erdos3.VectorPolynomial.forecastShortGridSheet_of_mixed line 326
  16. theorem OAI.Erdos3.VectorPolynomial.forecastShortGridNormalized_of_mixed line 332
  17. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridTest line 354
  18. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridTest_bounds line 361
  19. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridTest_eq_eval line 369
  20. theorem OAI.Erdos3.VectorPolynomial.forecastShortGridSheet_originalSample line 407
  21. theorem OAI.Erdos3.VectorPolynomial.forecastShortGridNormalized_originalSample line 419
  22. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridTest_originalSample_eq_eval line 438
  23. theorem OAI.Erdos3.VectorPolynomial.real_divisor_nsmul_circle line 483
  24. theorem OAI.Erdos3.VectorPolynomial.forecastNativeCoveredChart_commonCover_ambient line 506
  25. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.nativeSingleSiteCoverObservable_mixed_eq_forecastShortGridTest line 530
  26. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.nativeSingleSiteCoverObservable_normalized_raw_point line 562
  27. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridJointTest_bounds line 659
  28. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridJointTest_early_bounds line 678
  29. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridFullJointTest_bounds line 710
  30. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastShortGridFullJointTest_early_bounds line 726
  31. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.native_joint_modulus line 758