OAI/Combinatorics/Progressions/Sampling/ForecastRawSpatialBoxReorder.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.mixedCoveredJetDeckReference line 17
  2. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJetRawReference_prod line 22
  3. abbrev OAI.Erdos3.VectorPolynomial.ForecastSingleDeckResidues line 32
  4. theorem OAI.Erdos3.VectorPolynomial.forecastSingleMixedRawReference_eq line 40
  5. def OAI.Erdos3.VectorPolynomial.forecastSingleMixedRawEquiv line 44
  6. theorem OAI.Erdos3.VectorPolynomial.forecastSingleMixedRawEquiv_coe line 67
  7. def OAI.Erdos3.VectorPolynomial.forecastSingleMixedRawPoint line 73
  8. theorem OAI.Erdos3.VectorPolynomial.forecastSingleMixedRawEquiv_symm_apply line 78
  9. theorem OAI.Erdos3.VectorPolynomial.forecastSingleRawLayer_preserving line 84
  10. theorem OAI.Erdos3.VectorPolynomial.forecastSingleRawReal_flatten line 93
  11. theorem OAI.Erdos3.VectorPolynomial.forecastSingleRawInteger_flatten line 101
  12. theorem OAI.Erdos3.VectorPolynomial.forecastSingleRawArray_preserving line 111
  13. theorem OAI.Erdos3.VectorPolynomial.forecastSingleMixedRawEquiv_measurePreserving line 130
  14. theorem OAI.Erdos3.VectorPolynomial.forecastSingleMixedRaw_integral line 139
  15. theorem OAI.Erdos3.VectorPolynomial.forecastSingleMixedRaw_integrable_iff line 149
  16. theorem OAI.Erdos3.VectorPolynomial.uniform_complex_integral line 173
  17. def OAI.Erdos3.VectorPolynomial.forecastSingleDeckEquiv line 183
  18. theorem OAI.Erdos3.VectorPolynomial.forecastSingleDeckAverage line 190
  19. theorem OAI.Erdos3.VectorPolynomial.forecastSingleMixedRaw_normalized_split_integral line 226
  20. theorem OAI.Erdos3.VectorPolynomial.productGridReorder_preserving line 258
  21. def OAI.Erdos3.VectorPolynomial.forecastRawGridEquiv line 295
  22. theorem OAI.Erdos3.VectorPolynomial.forecastRawGridEquiv_measurePreserving line 337
  23. theorem OAI.Erdos3.VectorPolynomial.forecastRawGrid_integrable_iff line 347
  24. theorem OAI.Erdos3.VectorPolynomial.forecastRawGrid_integral line 357
  25. theorem OAI.Erdos3.VectorPolynomial.forecastRawGrid_rows_integrable_ae line 378
  26. theorem OAI.Erdos3.VectorPolynomial.forecastRawGrid_normalized_integral line 389
  27. theorem OAI.Erdos3.VectorPolynomial.productLeftComm_preserving line 420
  28. theorem OAI.Erdos3.VectorPolynomial.spatialGridReorder_preserving line 430
  29. theorem OAI.Erdos3.VectorPolynomial.integerSumCoordinates_preserving line 449
  30. def OAI.Erdos3.VectorPolynomial.forecastRawSpatialEquiv line 483
  31. theorem OAI.Erdos3.VectorPolynomial.forecastRawSpatialEquiv_measurePreserving line 540
  32. theorem OAI.Erdos3.VectorPolynomial.forecastRawSpatial_integral line 558
  33. theorem OAI.Erdos3.VectorPolynomial.forecastRawSpatialBox_normalized_integral line 595