OAI/MeasureTheory/Falconer/Slicing/GaussianActiveCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Active original tube-anchor counts in the Gaussian point parameter

  1. def OAI.Falconer.gaussianActiveAnchorCount line 13
  2. theorem OAI.Falconer.gaussianActiveAnchorCount_eq_sum line 18
  3. theorem OAI.Falconer.measurable_gaussianActiveAnchorCount line 25
  4. theorem OAI.Falconer.gaussianActiveAnchorCount_integral line 36
  5. theorem OAI.Falconer.gaussianActiveAnchorCount_exceptional line 49