WeightedTranslatedProfiles.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed polynomial weights absorb translations of normalized packet profiles. The estimates are uniform before all packet locations.

def OAI.LipschitzHilbert.PacketRepresentation.weightedTranslatedProfile line 10
theorem OAI.LipschitzHilbert.PacketRepresentation.translatedProfile_seminorm line 14
theorem OAI.LipschitzHilbert.PacketRepresentation.weightedTranslatedProfile_seminorm line 35
theorem OAI.LipschitzHilbert.PacketRepresentation.weightedTranslatedProfile_bounded line 63
Source documentation
Any fixed continuous seminorm has a uniformly weighted translation bound. Its finite required order determines the weight exponent.
```
theorem weightedTranslatedProfile_bounded (F : SchwartzMap (ℝ×ℝ) ℂ)
    (P : Seminorm ℝ (SchwartzMap (ℝ×ℝ) ℂ)) (hP : Continuous P) :
    ∃ q₀ : ℕ, ∃ C : ℝ, 0<C ∧ ∀ q : ℕ, q₀≤q → ∀ nu : SymbolSpace, ∀ a : ℝ×ℝ, ‖a‖≤‖nu‖ →
      P (weightedTranslatedProfile F q nu a)≤C := by
…
```
Mentions: OAI.LipschitzHilbert.PacketRepresentation.SymbolSpace, OAI.LipschitzHilbert.PacketRepresentation.weightedTranslatedProfile