OAI/Combinatorics/Progressions/Sampling/ForecastInactiveSlicedFixedProduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedSupportedPhysicalJointPMF line 35
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedPhysicalGrid_joint_law line 48
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedPhysicalGrid_joint_mass line 88
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedPhysicalGrid_joint_scaled_mass line 96
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedJointGrid_site_approximation line 134
  6. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_zero_axis_site_small_or_dense line 213
  7. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_product_site line 307