NormalizedSymbolRepresentation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier separation on the bounded frequency windows used for the annular packet decomposition. Constants precede both scale parameters.

theorem OAI.LipschitzHilbert.PacketRepresentation.symbolPoint_norm_le line 12

theorem OAI.LipschitzHilbert.PacketRepresentation.normalizedSchwartzSymbol_eq line 24

Source documentation

A cutoff which is one wherever the windowed annular symbol can be nonzero.

theorem normalizedSchwartzSymbol_eq (psi : SchwartzMap ℝ ℂ)
    (A B c M R : ℝ) (hR : 0<R) (hc : 0<c)
    (hpsi : ∀ s : ℝ, M < |s| → psi s=0)
    (hsize : A+B+(M+A)/c≤R)
    (v t X Y U : ℝ) (hp : ‖(v,t)‖≤R)
    (hX : |X|≤A) (hY : |Y|≤B) (hV : c≤v+t*Y) :
    normalizedSchwartzSymbol psi R hR v t (symbolPoint X Y U)=psi (X+(v+t*Y)*U) := by
…

Mentions: OAI.LipschitzHilbert.PacketRepresentation.normalizedSchwartzSymbol, OAI.LipschitzHilbert.PacketRepresentation.symbolPoint

def OAI.LipschitzHilbert.PacketRepresentation.symbolRadius line 44
theorem OAI.LipschitzHilbert.PacketRepresentation.symbolRadius_pos line 46

theorem OAI.LipschitzHilbert.PacketRepresentation.exists_normalized_symbol_representation line 53

Source documentation

The coefficient and weight bounds are uniform over every vertical bin and averaging scale satisfying the normalized annulus geometry.

theorem exists_normalized_symbol_representation (psi : SchwartzMap ℝ ℂ)
    (A B c C M : ℝ) (hA : 0≤A) (hB : 0≤B) (hc : 0<c) (hC : 0≤C) (hM : 0≤M)
    (hpsi : ∀ s : ℝ, M < |s| → psi s=0) (q : ℕ) :
    ∃ R : ℝ, ∃ hR : 0<R, ∃ D : ℝ, 0<D ∧
      (∀ v t : ℝ, ∀ nu : SymbolSpace, ∀ U : ℝ,
        ‖weightedSelector (normalizedSchwartzSymbol psi R hR v t) q nu U‖≤D*symbolWeight q nu) ∧
      (∀ v t X Y U : ℝ, |v|≤C → |t|≤1 → |X|≤A → |Y|≤B → c≤v+t*Y →
        psi (X+(v+t*Y)*U)=∫ nu : SymbolSpace,
          (symbolWeight q nu : ℂ)*((symbolWeight q nu : ℂ)*frequencyCharacter nu X Y)*
            (symbolWeight q nu : ℂ)*
              weightedSelector (normalizedSchwartzSymbol psi R hR v t) q nu U) := by
…

Mentions: OAI.LipschitzHilbert.PacketRepresentation.SymbolSpace, OAI.LipschitzHilbert.PacketRepresentation.weightedSelector, OAI.LipschitzHilbert.PacketRepresentation.normalizedSchwartzSymbol, OAI.LipschitzHilbert.PacketRepresentation.symbolWeight, OAI.LipschitzHilbert.PacketRepresentation.frequencyCharacter