OAI/MeasureTheory/Falconer/Fourier/SeparatedJets.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite separated symbols and their actual derivatives

The two external parameters remain in different factors. Directional derivatives use the ordinary product rule, so taking finitely many chart jets never introduces a joint endpoint symbol.

  1. structure OAI.Falconer.SmoothSeparation line 18
  2. def OAI.Falconer.SmoothSeparation.value line 30
  3. theorem OAI.Falconer.SmoothSeparation.value_contDiff line 33
  4. def OAI.Falconer.SmoothSeparation.product line 37
  5. theorem OAI.Falconer.SmoothSeparation.product_value line 47
  6. def OAI.Falconer.SmoothSeparation.mulLeft line 53
  7. theorem OAI.Falconer.SmoothSeparation.mulLeft_value line 62
  8. def OAI.Falconer.SmoothSeparation.pullback line 68
  9. theorem OAI.Falconer.SmoothSeparation.pullback_value line 77
  10. def OAI.Falconer.SmoothSeparation.derivative line 81
  11. theorem OAI.Falconer.SmoothSeparation.derivative_value line 98
  12. def OAI.Falconer.SmoothSeparation.sum line 119
  13. theorem OAI.Falconer.SmoothSeparation.sum_value line 128
  14. def OAI.Falconer.SmoothSeparation.laplacian line 134
  15. theorem OAI.Falconer.SmoothSeparation.laplacian_value line 138
  16. def OAI.Falconer.SmoothSeparation.iteratedLaplacian line 156
  17. theorem OAI.Falconer.SmoothSeparation.iteratedLaplacian_value line 160