OAI/MeasureTheory/Falconer/Geometry/SeparationOrder.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The total 2j derivative budget in the actual finite inverse split

  1. def OAI.Falconer.SmoothSeparation.HasOrder line 19
  2. theorem OAI.Falconer.SmoothSeparation.HasOrder.mono line 23
  3. theorem OAI.Falconer.SmoothSeparation.product_hasOrder line 29
  4. theorem OAI.Falconer.SmoothSeparation.HasOrder.mulLeft line 36
  5. theorem OAI.Falconer.SmoothSeparation.HasOrder.pullback line 43
  6. theorem OAI.Falconer.SmoothSeparation.HasOrder.derivative line 49
  7. theorem OAI.Falconer.SmoothSeparation.sum_hasOrder line 59
  8. theorem OAI.Falconer.SmoothSeparation.HasOrder.laplacian line 65
  9. theorem OAI.Falconer.SmoothSeparation.HasOrder.iteratedLaplacian line 70
  10. theorem OAI.Falconer.SmoothSeparation.HasOrder.stationaryJet line 80
  11. theorem OAI.Falconer.SmoothSeparation.HasOrder.inverse line 88
  12. theorem OAI.Falconer.localInverseAmplitude_product_separated_order line 107