OAI/MeasureTheory/Falconer/Fourier/MaskJetAlgebra.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Finite algebra of individual ambient mask jets

A term contains each original mask exactly once, evaluated at one smooth angular chart point, with a fixed finite jet on each occurrence. The coefficient contains only the fixed chart geometry. Differentiation can therefore distribute to one mask without deleting any other occurrence.

  1. structure OAI.Falconer.MaskJetIndex line 22
  2. def OAI.Falconer.MaskJetIndex.zero line 29
  3. def OAI.Falconer.MaskJetIndex.prepend line 32
  4. def OAI.Falconer.MaskJetIndex.value line 36
  5. theorem OAI.Falconer.MaskJetIndex.zero_value line 39
  6. theorem OAI.Falconer.MaskJetIndex.value_contDiff line 42
  7. theorem OAI.Falconer.MaskJetIndex.fderiv_value line 47
  8. theorem OAI.Falconer.complex_clm_coordinate_expansion line 58
  9. theorem OAI.Falconer.MaskJetIndex.fderiv_comp line 65
  10. structure OAI.Falconer.MaskJetTerm line 82
  11. def OAI.Falconer.MaskJetTerm.value line 95
  12. def OAI.Falconer.MaskJetTerm.order line 99
  13. theorem OAI.Falconer.MaskJetTerm.value_contDiff line 101
  14. def OAI.Falconer.MaskJetTerm.mulFixed line 106
  15. theorem OAI.Falconer.MaskJetTerm.mulFixed_value line 110
  16. def OAI.Falconer.MaskJetTerm.pullback line 115
  17. theorem OAI.Falconer.MaskJetTerm.pullback_value line 119
  18. def OAI.Falconer.MaskJetTerm.derivativeTerm line 123
  19. theorem OAI.Falconer.MaskJetTerm.derivativeTerm_order line 136
  20. theorem OAI.Falconer.MaskJetTerm.fderiv_product line 152
  21. theorem OAI.Falconer.MaskJetTerm.derivativeTerm_value_right line 161
  22. theorem OAI.Falconer.MaskJetTerm.derivative_value line 184