OAI/MeasureTheory/Falconer/Measures/SeparatedSupport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Support bookkeeping for separated angular derivatives

The anchor maps track the point of the original endpoint symbol sampled by each factor. Differentiation cannot enlarge support, while a chart substitution pulls it back along its continuous anchor map.

  1. structure OAI.Falconer.SeparationSupport line 22
  2. def OAI.Falconer.SeparationSupport.At line 32
  3. def OAI.Falconer.SeparationSupport.product line 36
  4. def OAI.Falconer.SeparationSupport.mulLeft line 46
  5. def OAI.Falconer.SeparationSupport.pullback line 56
  6. def OAI.Falconer.SeparationSupport.derivative line 68
  7. def OAI.Falconer.SeparationSupport.sum line 85
  8. def OAI.Falconer.SeparationSupport.laplacian line 95
  9. theorem OAI.Falconer.SeparationSupport.derivative_at line 100
  10. theorem OAI.Falconer.SeparationSupport.laplacian_at line 106
  11. theorem OAI.Falconer.SeparationSupport.iteratedLaplacian line 112
  12. theorem OAI.Falconer.SeparationSupport.left_mem_of_ne_zero line 123
  13. theorem OAI.Falconer.SeparationSupport.right_mem_of_ne_zero line 130
  14. theorem OAI.Falconer.SeparationSupport.stationaryJet line 137
  15. theorem OAI.Falconer.SeparationSupport.inverse line 159
  16. theorem OAI.Falconer.localInverseAmplitude_product_factors line 184