OAI/MeasureTheory/Falconer/Estimates/FinitePartitionMask.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded measurable masks on a finite disjoint spatial partition

  1. def OAI.Falconer.finitePartitionMask line 11
  2. theorem OAI.Falconer.finitePartitionMask_measurable line 14
  3. theorem OAI.Falconer.finitePartitionMask_on line 20
  4. theorem OAI.Falconer.finitePartitionMask_off line 34
  5. theorem OAI.Falconer.finitePartitionMask_bounds line 41