OAI/Combinatorics/Progressions/Sampling/ForecastActiveGridIntegralComparison.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoinEquiv line 25
  2. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoinEquiv_apply line 32
  3. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoinEquiv_coe line 44
  4. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoinEquiv_measurePreserving line 50
  5. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_measurePreserving line 59
  6. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_integrable_iff line 67
  7. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_integral line 76
  8. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_iterated_integral line 85
  9. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_integral_integrable line 92
  10. theorem OAI.Erdos3.VectorPolynomial.forecastActive_density_test_grid_quadrature line 120
  11. def OAI.Erdos3.VectorPolynomial.forecastJointAxisEquiv line 198
  12. def OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoinEquiv line 218
  13. def OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin line 225
  14. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoinEquiv_apply line 231
  15. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoinEquiv_measurePreserving line 246
  16. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin_isometry line 256
  17. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin_lipschitz line 271
  18. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin_zero line 277
  19. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin_norm line 285
  20. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin_integrable_iff line 291
  21. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin_integral line 300
  22. theorem OAI.Erdos3.VectorPolynomial.forecastJointCoordinateJoin_iterated_integral line 308
  23. theorem OAI.Erdos3.VectorPolynomial.forecastActive_density_test_integral_comparison line 338
  24. theorem OAI.Erdos3.VectorPolynomial.forecastActive_density_test_reference_comparison line 383