OAI/Combinatorics/Progressions/Dynamics/AllocatedFixedPathRationalComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_crtRationalForecast_reference line 39
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_full_principal_residue_riemann line 120
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_rational_forecast_comparison line 203