OAI/Combinatorics/Progressions/Probability/ScaledCubeProductMeasure.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scalarCubeProductDomain line 13
  2. def OAI.Erdos3.scalarCubeProductMeasure line 16
  3. instance OAI.Erdos3.scalarCubeProductMeasure_probability line 20
  4. theorem OAI.Erdos3.scalarCubeProductMeasure_eq_closed line 25
  5. theorem OAI.Erdos3.scalarCubeProductMeasure_eq_smul_restrict line 30
  6. theorem OAI.Erdos3.scalarCubeProductMeasure_integral line 44
  7. theorem OAI.Erdos3.scalarCubeProductMeasure_ae_domain line 53
  8. theorem OAI.Erdos3.unitBoxMeasure_eq_pi line 76
  9. theorem OAI.Erdos3.scalarOneCube_product_endpoints line 82
  10. theorem OAI.Erdos3.scalarOneCube_product_image line 97
  11. def OAI.Erdos3.scaledScalarCubeMeasure line 118
  12. theorem OAI.Erdos3.scaledScalarCubeMeasure_eq_map line 122
  13. theorem OAI.Erdos3.scaledScalarCubeMeasure_probability line 139
  14. theorem OAI.Erdos3.scaledScalarCubeMeasure_normalize line 144
  15. theorem OAI.Erdos3.scaledScalarCubeMeasure_integral line 155
  16. theorem OAI.Erdos3.scaledScalarCubeMeasure_ae_domain line 161
  17. theorem OAI.Erdos3.scalarCubeDomain_empty line 179
  18. theorem OAI.Erdos3.scalarCubeDomain_empty_volume line 190
  19. theorem OAI.Erdos3.scalarCubeMeasure_empty_map line 196
  20. theorem OAI.Erdos3.scalarCubeProductMeasure_empty_map line 204
  21. theorem OAI.Erdos3.scalarCubeProductMeasure_empty_integral line 213
  22. def OAI.Erdos3.scaledClosedCubeDomain line 231
  23. theorem OAI.Erdos3.scaledClosedCubeDomain_smul_iff line 235
  24. theorem OAI.Erdos3.scaledClosedCubeDomain_eq_image line 243
  25. theorem OAI.Erdos3.scaledScalarCubeMeasure_eq_closed line 255
  26. def OAI.Erdos3.scaledCubeProductMeasure line 285
  27. theorem OAI.Erdos3.scaledCubeProductMeasure_eq_map line 290
  28. theorem OAI.Erdos3.scaledCubeProductMeasure_probability line 303
  29. theorem OAI.Erdos3.scaledCubeProductMeasure_eq_smul_restrict line 311