OAI/Combinatorics/Progressions/Dynamics/AllocatedFixedPathSlicedNativeAmbientComparison.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_kernel_geometry line 24
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_principal_geometry line 45
  3. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalForecastDensity line 186
  4. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalSourceMean line 196
  5. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalRationalMean line 219
  6. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalResidueMean line 234
  7. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalComparisonError line 247
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalSourceMean_residue_comparison line 269
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalResidueMean_eq_rationalMean line 290
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_physical_rational_density_comparison line 300
  11. def OAI.Erdos3.VectorPolynomial.allocatedSlicedNativeEvalMean line 403
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalSourceMean_eq_native line 420
  13. def OAI.Erdos3.allocatedFixedPathSlicedAmbientFloorLog line 450
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalComparisonError_eq_sourceError line 463
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedFixedPathSlicedUniformPrecision line 478
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_native_test_rational_comparison line 696
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_recovered_native_rational_comparison line 728
  18. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalAmbientMean line 954
  19. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalAmbientGridError line 957
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_ambient_rational_comparison line 983
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_native_ambient_comparison line 1237