OAI/Combinatorics/Progressions/Estimates/ActualFiberSlicedBoundedTwistPrecision.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedFiberActiveProgression_common_contained line 46
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedFiberActiveContainedProgression_eq_common line 54
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedFiberPhysicalRoot_eq_raw line 72
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedFiberSliceLaw_native_complexMean line 92
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedChildFiber_active_length line 142
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedChildFiberSliceLaw_native_complexMean line 156
  7. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.toDenseSliceMember_nativeMean line 230
  8. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.denseFiber_ambient_model_comparison line 384
  9. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.denseFiber_ambient_model_precision line 530
  10. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.denseFiber_ambient_early_model_precision line 701
  11. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.denseFiber_ambient_constructed_late_precision line 847
  12. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.denseFiber_ambient_original_twist_precision line 994
  13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.denseFiber_ambient_original_star_twist_precision line 1024
  14. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.denseFiber_ambient_bounded_original_twist_precision line 1185