OAI/Combinatorics/Progressions/Estimates/CoefficientJetScalar.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.CoefficientAxisRow line 13
  2. instance OAI.Erdos3.VectorPolynomial.coefficientAxisRowMeasurable line 18
  3. abbrev OAI.Erdos3.VectorPolynomial.CoefficientAxisArrays line 24
  4. def OAI.Erdos3.VectorPolynomial.coefficientAxisEquiv line 27
  5. theorem OAI.Erdos3.VectorPolynomial.coefficientAxisEquiv_continuous line 33
  6. theorem OAI.Erdos3.VectorPolynomial.coefficientAxisEquiv_integer line 37
  7. def OAI.Erdos3.VectorPolynomial.coefficientAxisLaw line 45
  8. theorem OAI.Erdos3.VectorPolynomial.coefficientAxisLaw_probability line 50
  9. theorem OAI.Erdos3.VectorPolynomial.coefficientAxisEquiv_measurePreserving line 64
  10. def OAI.Erdos3.VectorPolynomial.coefficientAxisSplitEquiv line 87
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientAxisSplitEquiv_symm_left line 94
  12. theorem OAI.Erdos3.VectorPolynomial.coefficientAxisSplitEquiv_symm_right line 101
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientAxisSplitEquiv_measurePreserving line 108
  14. def OAI.Erdos3.VectorPolynomial.CoefficientJetAxisRow line 131
  15. instance OAI.Erdos3.VectorPolynomial.coefficientJetAxisRowMeasurable line 135
  16. def OAI.Erdos3.VectorPolynomial.coefficientJetAxisReference line 141
  17. instance OAI.Erdos3.VectorPolynomial.coefficientJetAxisReference_sigmaFinite line 146
  18. def OAI.Erdos3.VectorPolynomial.coefficientJetAxisMap line 157
  19. theorem OAI.Erdos3.VectorPolynomial.coefficientJetAxisMap_measurable line 163
  20. def OAI.Erdos3.VectorPolynomial.coefficientJetRowReindex line 187
  21. theorem OAI.Erdos3.VectorPolynomial.coefficientJetRowReindex_measurePreserving line 195
  22. def OAI.Erdos3.VectorPolynomial.coefficientJetRowsReindex line 207
  23. theorem OAI.Erdos3.VectorPolynomial.coefficientJetRowsReindex_measurePreserving line 214
  24. def OAI.Erdos3.VectorPolynomial.CoefficientJetScalar line 232
  25. instance OAI.Erdos3.VectorPolynomial.coefficientJetScalarMeasurable line 236
  26. def OAI.Erdos3.VectorPolynomial.coefficientJetScalarReference line 242
  27. instance OAI.Erdos3.VectorPolynomial.coefficientJetScalarReference_sigmaFinite line 247
  28. def OAI.Erdos3.VectorPolynomial.coefficientJetScalarEquiv line 255
  29. theorem OAI.Erdos3.VectorPolynomial.coefficientJetScalarEquiv_measurePreserving line 261