SincMaskedLine.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact sinc-masked synthesis waves retain the analyzing budget and have a factor-two envelope constant when their derivative bandwidth is at most the packet's inverse length.

theorem OAI.LipschitzHilbert.LinePacketFamily.sincMasked_bound line 20
theorem OAI.LipschitzHilbert.LinePacketFamily.sincMasked_deriv line 29
def OAI.LipschitzHilbert.LinePacketFamily.sincMasked line 53
Source documentation
Only the synthesis waves change. Coefficients and all lattice geometry are retained literally.
```
def sincMasked
    (hband : ∀ j u k, 2*(n:ℝ)*(|a j u k|+|c j u k|) ≤ 1/P.length j) :
    LinePacketFamily N κ ι :=
…
```
Mentions: OAI.LipschitzHilbert.LinePacketFamily
theorem OAI.LipschitzHilbert.LinePacketFamily.sincMasked_coeff line 62
theorem OAI.LipschitzHilbert.LinePacketFamily.sincMasked_wave line 65
theorem OAI.LipschitzHilbert.LinePacketFamily.sincMasked_budget line 70

theorem OAI.LipschitzHilbert.LinePacketFamily.sincMasked_cutoffs line 74

Source documentation

Uniform annuli are weakened by precisely the mask bandwidth.

theorem sincMasked_cutoffs (lo hi delta : ℝ)
    (hdelta : ∀ j u k, (2*(n:ℝ))*((|a j u k|+|c j u k|)/(2*Real.pi)) ≤ delta*(2:ℝ)^j.val)
    (hlow : ∀ j u k xi, |xi| < lo*(2:ℝ)^j.val → 𝓕 (P.wave j u k) xi = 0)
    (hhigh : ∀ j u k xi, hi*(2:ℝ)^j.val < |xi| → 𝓕 (P.wave j u k) xi = 0) :
    (∀ j u k xi, |xi| < (lo-delta)*(2:ℝ)^j.val →
      𝓕 ((P.sincMasked n a b c d hband).wave j u k) xi = 0) ∧
    (∀ j u k xi, (hi+delta)*(2:ℝ)^j.val < |xi| →
      𝓕 ((P.sincMasked n a b c d hband).wave j u k) xi = 0) := by
…