OAI/MeasureTheory/Falconer/Fourier/MaskJetGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite family for the inverse's geometric coefficients

Changing which mask receives a derivative changes its jet index, but not the smooth coefficient or evaluation point. Collapse all mask choices to one label to obtain a coefficient family independent of the list length.

  1. def OAI.Falconer.MaskJetExpansion.GeometryCoveredBy line 18
  2. theorem OAI.Falconer.MaskJetExpansion.product_geometryCoveredBy line 23
  3. theorem OAI.Falconer.MaskJetExpansion.GeometryCoveredBy.mulFixed line 28
  4. theorem OAI.Falconer.MaskJetExpansion.GeometryCoveredBy.pullback line 40
  5. theorem OAI.Falconer.MaskJetExpansion.sum_geometryCoveredBy line 55
  6. theorem OAI.Falconer.MaskJetExpansion.GeometryCoveredBy.derivative line 62
  7. theorem OAI.Falconer.MaskJetExpansion.GeometryCoveredBy.laplacian line 85
  8. theorem OAI.Falconer.MaskJetExpansion.GeometryCoveredBy.iteratedLaplacian line 91
  9. theorem OAI.Falconer.MaskJetExpansion.GeometryCoveredBy.stationaryJet line 101
  10. theorem OAI.Falconer.MaskJetExpansion.GeometryCoveredBy.inverse line 111
  11. theorem OAI.Falconer.MaskJetExpansion.inverse_product_geometryCoveredBy_unit line 128
  12. theorem OAI.Falconer.MaskJetExpansion.coefficient_derivatives_bounded_on line 134
  13. theorem OAI.Falconer.MaskJetExpansion.inverse_product_coefficient_derivatives line 149

    Source documentation

    The coefficient bound is selected before the finite mask type.

    theorem inverse_product_coefficient_derivatives (m j k : ℕ)
    {s : Set (Space (m+3))} (hs : IsCompact s) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (ι : Type) [Fintype ι] [DecidableEq ι],
      ∀ a : ((product : MaskJetExpansion ι (m+3) (Space (m+3))).inverse m j).index,
        ∀ z ∈ s, ‖iteratedFDeriv ℝ k
          ((((product : MaskJetExpansion ι (m+3) (Space (m+3))).inverse m j).term a).coefficient)
          z‖ ≤ C := by
…

    Mentions: OAI.Falconer.Space, OAI.Falconer.MaskJetExpansion.product, OAI.Falconer.MaskJetExpansion, OAI.Falconer.MaskJetExpansion.inverse