OAI/Combinatorics/Progressions/Estimates/MixedCoveredRowReindex.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.mixedCoveredJetEquiv line 20
  2. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJetEquiv_apply line 30
  3. def OAI.Erdos3.VectorPolynomial.coveredJetArrayReference line 51
  4. theorem OAI.Erdos3.VectorPolynomial.coveredJetArrayReference_eq_smul line 63
  5. theorem OAI.Erdos3.VectorPolynomial.coveredJetArrayReference_sigmaFinite line 75
  6. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJetEquiv_measurePreserving line 88
  7. def OAI.Erdos3.VectorPolynomial.coveredJetArrayScale line 137
  8. theorem OAI.Erdos3.VectorPolynomial.coveredJetArrayScale_pos line 144
  9. theorem OAI.Erdos3.VectorPolynomial.coveredJetArrayReference_eq_real_smul line 149
  10. theorem OAI.Erdos3.VectorPolynomial.coveredJetArrayReference_density line 164
  11. theorem OAI.Erdos3.count_isOpenPosMeasure line 189
  12. theorem OAI.Erdos3.uniformPMF_isOpenPosMeasure line 199
  13. theorem OAI.Erdos3.normalizedCoveredReference_isOpenPosMeasure line 210
  14. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJetEquiv_continuous line 232
  15. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJetEquiv_symm_continuous line 240
  16. theorem OAI.Erdos3.VectorPolynomial.coveredJetSourceRegion_isOpen line 248
  17. theorem OAI.Erdos3.VectorPolynomial.coveredJetReference_isOpenPosMeasure line 258
  18. def OAI.Erdos3.VectorPolynomial.mixedCoveredRowsReindex line 283
  19. def OAI.Erdos3.VectorPolynomial.euclideanJetRowsReindex line 294
  20. theorem OAI.Erdos3.VectorPolynomial.euclideanJetRowsReindex_measurePreserving line 301
  21. theorem OAI.Erdos3.VectorPolynomial.coveredJetArrayScale_reindex_rows line 311
  22. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJetChart_reindex_rows line 324
  23. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredJetRegion_reindex_rows line 330