OAI/Combinatorics/Progressions/Lattices/AllocatedAffineFixedPathRationalReference.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rationalInactivePolynomialForecast_arbitraryStepCRT_tsum_marginal line 19
  2. def OAI.Erdos3.VectorPolynomial.allocatedInactiveAffineIntervalLaw line 72
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveAffineIntervalLaw_complexMean line 80
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveAffineIntervalLaw_total line 87
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveAffineIntervalLaw_fixed_grid_mean line 97
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveAffineIntervalLaw_fixed_grid_law line 116
  7. def OAI.Erdos3.VectorPolynomial.allocatedAffineIntervalInactiveForecast line 138
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineIntervalInactiveForecast_mass_one line 148
  9. def OAI.Erdos3.VectorPolynomial.allocatedJointResidueOutput line 190
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedJointResidueOutput_join line 202
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedJointResidueOutput_actual line 228
  12. theorem OAI.Erdos3.VectorPolynomial.affineReference_uniform_sum_flip line 270
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineFixedPath_crtRationalForecast_reference line 321
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineFixedPath_joint_crtRationalForecast_reference line 384