OAI/MeasureTheory/Falconer/Fourier/MaskJetSeed.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Starting the inverse expansion with existing individual mask jets

Previously charged derivatives remain in their original occurrences. The new inverse adds at most twice its index to the total order, and radius normalization cancels every previously charged power exactly.

  1. def OAI.Falconer.MaskJetExpansion.seed line 18
  2. theorem OAI.Falconer.MaskJetExpansion.seed_value line 24
  3. theorem OAI.Falconer.MaskJetExpansion.seed_hasOrder line 31
  4. theorem OAI.Falconer.MaskJetExpansion.seed_hasPointAt line 35
  5. theorem OAI.Falconer.MaskJetExpansion.seed_geometryCoveredBy_unit line 39
  6. def OAI.Falconer.MaskJetExpansion.OrdersExtend line 43
  7. theorem OAI.Falconer.MaskJetExpansion.seed_ordersExtend line 47
  8. theorem OAI.Falconer.MaskJetExpansion.OrdersExtend.mulFixed line 51
  9. theorem OAI.Falconer.MaskJetExpansion.OrdersExtend.pullback line 56
  10. theorem OAI.Falconer.MaskJetExpansion.sum_ordersExtend line 61
  11. theorem OAI.Falconer.MaskJetExpansion.OrdersExtend.derivative line 65
  12. theorem OAI.Falconer.MaskJetExpansion.OrdersExtend.laplacian line 80
  13. theorem OAI.Falconer.MaskJetExpansion.OrdersExtend.iteratedLaplacian line 85
  14. theorem OAI.Falconer.MaskJetExpansion.OrdersExtend.stationaryJet line 94
  15. theorem OAI.Falconer.MaskJetExpansion.OrdersExtend.inverse line 103
  16. theorem OAI.Falconer.MaskJetExpansion.seed_inverse_added_order line 119
  17. theorem OAI.Falconer.MaskJetExpansion.radius_power_cancel line 134
  18. theorem OAI.Falconer.MaskJetExpansion.seed_inverse_radius_cancel line 142
  19. theorem OAI.Falconer.MaskJetExpansion.seed_inverse_radius_le line 152