OAI/Combinatorics/Progressions/Probability/ScalarCubeHistogramMeasure.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FiniteProbabilityWeights.imageMeasure line 14
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.imageMeasure_probability line 18
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.imageMeasure_apply line 25
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.imageMeasure_integral line 34
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.imageMeasure_pi line 54
  6. def OAI.Erdos3.scalarCubeProbabilityDensity line 88
  7. def OAI.Erdos3.scalarCubeGridDensity line 91
  8. theorem OAI.Erdos3.scalarCubeProbabilityDensity_measurable line 95
  9. theorem OAI.Erdos3.scalarCubeProbabilityDensity_spec line 101
  10. theorem OAI.Erdos3.scalarCubeProbabilityDensity_measure line 110
  11. theorem OAI.Erdos3.scalarCubeGridDensity_measurable line 120
  12. theorem OAI.Erdos3.scalarCubeGridDensity_spec line 132
  13. theorem OAI.Erdos3.scalarCubeResidue_imageMeasure line 144