OAI/Analysis/LipschitzHilbert/Fourier/SymbolSlice.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Restricting one fixed Schwartz symbol to the two scale parameters. The restriction does not enlarge any Schwartz seminorm.

  1. abbrev OAI.LipschitzHilbert.PacketRepresentation.MasterSymbolSpace line 12
  2. def OAI.LipschitzHilbert.PacketRepresentation.symbolInclusion line 14
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolInclusion_norm line 17
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolSlice_temperate line 20
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolSlice_antilipschitz line 28
  6. def OAI.LipschitzHilbert.PacketRepresentation.symbolSlice line 35
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolSlice_apply line 40
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolSlice_derivative_bound line 43
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolSlice_seminorm line 62
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolSlice_coefficient_uniform line 77

    Source documentation

    The Fourier coefficient bound is uniform over both parameters. Only finitely many seminorms of the single master symbol enter.

    theorem symbolSlice_coefficient_uniform (F : SchwartzMap MasterSymbolSpace ℂ) (q : ℕ) :
    ∃ C : ℝ, 0<C ∧ ∀ p : ℝ × ℝ, symbolCoefficientBound (symbolSlice F p) q≤C := by
…

    Mentions: OAI.LipschitzHilbert.PacketRepresentation.MasterSymbolSpace, OAI.LipschitzHilbert.PacketRepresentation.symbolCoefficientBound, OAI.LipschitzHilbert.PacketRepresentation.symbolSlice