OAI/Combinatorics/Progressions/Sampling/AllocatedFixedPathRecoveredJointGridComparison.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.forecastCongruenceJointAxisEquiv line 23
  2. theorem OAI.Erdos3.VectorPolynomial.forecastCongruenceJointAxisEquiv_output line 44
  3. theorem OAI.Erdos3.VectorPolynomial.forecastCongruenceJointAxisEquiv_merged_output line 53
  4. theorem OAI.Erdos3.VectorPolynomial.forecastCongruenceJointAxisEquiv_merged_output_mod line 67
  5. theorem OAI.Erdos3.VectorPolynomial.forecastCongruenceJointAxis_card line 84
  6. theorem OAI.Erdos3.VectorPolynomial.forecastCongruenceJointAxis_card_le line 91
  7. theorem OAI.Erdos3.VectorPolynomial.forecastCongruenceJointAxis_rationalInactiveForecast line 97
  8. theorem OAI.Erdos3.VectorPolynomial.forecastJoint_rational_reference line 143
  9. def OAI.Erdos3.VectorPolynomial.forecastJointOriginalGridMean line 216
  10. theorem OAI.Erdos3.VectorPolynomial.forecastJointOriginalGridMean_reindexed line 227
  11. theorem OAI.Erdos3.VectorPolynomial.forecastJointOriginalGridMean_reindexed_comparison line 294
  12. theorem OAI.Erdos3.VectorPolynomial.forecastJointOriginalGridMean_comparison line 352
  13. theorem OAI.Erdos3.VectorPolynomial.forecastJointOriginalGridMean_mul_normalization line 442
  14. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialNativeJointGridMean_comparison line 514
  15. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialSliceNativeJointGridMean_comparison line 646
  16. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialNativeJointGridMean_precision line 774
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredNativeJointGridMean_precision line 897
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_recovered_native_jointGrid_comparison line 1058