OAI/MeasureTheory/Falconer/Shells/RootShellData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PlanarFalconer.RootShellData line 9
  2. def OAI.PlanarFalconer.RootShellData.indices line 19
  3. def OAI.PlanarFalconer.RootShellData.endpointLeft line 20
  4. def OAI.PlanarFalconer.RootShellData.endpointRight line 21
  5. def OAI.PlanarFalconer.RootShellData.coefficient line 22
  6. def OAI.PlanarFalconer.RootShellData.mainF line 24
  7. def OAI.PlanarFalconer.RootShellData.measure line 25
  8. def OAI.PlanarFalconer.RootShellData.cost line 26
  9. theorem OAI.PlanarFalconer.RootShellData.endpointLeft_measurable line 29
  10. theorem OAI.PlanarFalconer.RootShellData.endpointRight_measurable line 33
  11. theorem OAI.PlanarFalconer.RootShellData.endpointLeft_norm line 37
  12. theorem OAI.PlanarFalconer.RootShellData.endpointRight_norm line 42
  13. theorem OAI.PlanarFalconer.RootShellData.coefficient_norm line 47