OAI/MeasureTheory/Falconer/Measures/DescriptorProduct.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual descriptor products and their reached angular factors

  1. def OAI.Falconer.descriptorProduct line 14
  2. theorem OAI.Falconer.descriptorProduct_measurable line 19
  3. theorem OAI.Falconer.descriptorProduct_bounds line 25
  4. theorem OAI.Falconer.descriptorProduct_support line 39
  5. theorem OAI.Falconer.uniform_descriptorProduct_core line 49
  6. theorem OAI.Falconer.descriptorProduct_pair_support line 67
  7. theorem OAI.Falconer.descriptorMask_reached_on_cell line 81
  8. theorem OAI.Falconer.descriptorProduct_reached_split line 99
  9. theorem OAI.Falconer.endpointTransform_descriptorProduct_split line 121