OAI/MeasureTheory/Falconer/Slicing/SliceNormalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Normalizing the retained original-label slice laws

  1. def OAI.Falconer.normalizedSliceLaw line 13
  2. theorem OAI.Falconer.normalizedSliceLaw_apply line 18
  3. theorem OAI.Falconer.normalizedSliceLaw_bound line 22
  4. theorem OAI.Falconer.normalizedSliceLaw_ae line 29
  5. theorem OAI.Falconer.positive_incidence_marginals line 34
  6. theorem OAI.Falconer.incidence_marginal_lower_bounds line 44
  7. theorem OAI.Falconer.normalizedSliceLaw_incidence line 62
  8. theorem OAI.Falconer.normalizedSliceLaw_incidence_lower line 71