OAI/MeasureTheory/Falconer/Angular/BadDirectionEnvelope.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A Borel envelope for geometric bad directions

The finite anchor net and the envelope depend only on the point law and the geometric test, before a direction measure is selected.

  1. def OAI.Falconer.boundedTubeUnion line 16
  2. theorem OAI.Falconer.boundedTubeUnion_joint_measurable line 20
  3. theorem OAI.Falconer.boundedTubeUnion_mass_measurable line 42
  4. def OAI.Falconer.finiteBadDirections line 47
  5. theorem OAI.Falconer.finiteBadDirections_measurable line 51
  6. theorem OAI.Falconer.original_bad_direction_mem_envelope line 65