NormalizedSymbolFormL1.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original finite normalized symbol form equals the common weighted average of the actual normalized convolution forms.

def OAI.LipschitzHilbert.PacketRepresentation.normalizedSymbolSumL1 line 15
theorem OAI.LipschitzHilbert.PacketRepresentation.normalized_symbol_sum_eq_average_l1 line 32

theorem OAI.LipschitzHilbert.PacketRepresentation.normalized_symbol_sum_bound_l1 line 70

Source documentation

A bound for the entire normalized convolution sum passes through the same common Fourier weight to the original finite symbol form.

theorem normalized_symbol_sum_bound_l1
    (chiA chiB : SchwartzMap (ℝ×ℝ) ℂ) (chi : SchwartzMap ℝ ℝ)
    (hchi : ∀ s, |chi s|≤1) (C : ℝ) (hC : 0<C) (q : ℕ) (hq : 4≤q)
    (topLength width w : ℝ) (htop : 0<topLength) (hwidth : 0<width)
    (labels : ∀ j, Finset (Label j)) (theta : ∀ j, labels j → ℝ) (center : κ → ℝ)
    (S : LatticeRow labels → κ → SchwartzMap SymbolSpace ℂ)
    (hS : ∀ i k, symbolCoefficientBound (S i k) q≤C)
    (u : ℝ×ℝ → ℝ) (hu : Measurable u)
    (f : κ → ℝ×ℝ → ℂ) (fData g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (hfint : ∀ k, Integrable (f k) planeMeasure)
    (hf : ∀ z k, f k z=fData z k) (hg : Measurable g)
    (hgint : ∀ k, Integrable (fun z => g z k) planeMeasure) (bound : ℝ)
…

Mentions: OAI.LipschitzHilbert.PacketRepresentation.LatticeRow, OAI.LipschitzHilbert.PacketRepresentation.SymbolSpace, OAI.LipschitzHilbert.PacketRepresentation.symbolCoefficientBound, OAI.LipschitzHilbert.PacketRepresentation.planeMeasure