OAI/MeasureTheory/Falconer/Measures/AmbientProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Ambient products preserve every original descriptor support

  1. def OAI.Falconer.descriptorAmbientProduct line 13
  2. theorem OAI.Falconer.descriptorAmbientProduct_sphere line 19
  3. theorem OAI.Falconer.descriptorAmbientProduct_contDiff line 26
  4. theorem OAI.Falconer.descriptorAmbientProduct_measurable line 33
  5. theorem OAI.Falconer.descriptorAmbientProduct_reached_on_cell line 40
  6. theorem OAI.Falconer.descriptorAmbientProduct_tsupport_good line 66
  7. theorem OAI.Falconer.descriptorAmbientProduct_derivative_good line 81
  8. theorem OAI.Falconer.descriptorAmbientProduct_complex_tsupport_good line 90