SincMaskSchwartz.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Smooth sinc multipliers preserve Schwartz packets. The derivative bounds follow from the same compact cosine average used for the mask's Fourier support; no assertion about a singular quotient at zero is used.

def OAI.LipschitzHilbert.sincJet line 17
theorem OAI.LipschitzHilbert.sincJet_integrand_bound line 20
theorem OAI.LipschitzHilbert.sincJet_integrable line 26
theorem OAI.LipschitzHilbert.sincJet_bound line 35
theorem OAI.LipschitzHilbert.sincJet_continuous line 43
theorem OAI.LipschitzHilbert.sincJet_hasDerivAt line 53
theorem OAI.LipschitzHilbert.sincJet_deriv line 83
theorem OAI.LipschitzHilbert.sincJet_contDiff line 87
theorem OAI.LipschitzHilbert.sincJet_zero line 99
theorem OAI.LipschitzHilbert.sincJet_iteratedDeriv line 104
theorem OAI.LipschitzHilbert.norm_iteratedDeriv_sinc_le_one line 110
Source documentation
All real sinc derivatives are uniformly bounded by one.
```
theorem norm_iteratedDeriv_sinc_le_one (n : ℕ) (x : ℝ) :
    ‖iteratedDeriv n Real.sinc x‖ ≤ 1 := by
…
```
theorem OAI.LipschitzHilbert.sinc_hasTemperateGrowth line 115
theorem OAI.LipschitzHilbert.affineSinc_hasTemperateGrowth line 122
def OAI.LipschitzHilbert.affineSincSchwartz line 128
Source documentation
The genuine affine sinc multiplier applied to a Schwartz packet.
```
def affineSincSchwartz (f : SchwartzMap ℝ ℂ) (a b : ℝ) : SchwartzMap ℝ ℂ :=
…
```
theorem OAI.LipschitzHilbert.affineSincSchwartz_apply line 131
theorem OAI.LipschitzHilbert.sincProductAffine_hasTemperateGrowth line 135
def OAI.LipschitzHilbert.sincProductSchwartz line 143
Source documentation
Multiplication by the actual even mask is a Schwartz operation.
```
def sincProductSchwartz (f : SchwartzMap ℝ ℂ) (n : ℕ) (a b c d : ℝ) : SchwartzMap ℝ ℂ :=
…
```
theorem OAI.LipschitzHilbert.sincProductSchwartz_apply line 147
theorem OAI.LipschitzHilbert.sincProductSchwartz_norm_le line 153
theorem OAI.LipschitzHilbert.sincProductAffine_lipschitz line 160

theorem OAI.LipschitzHilbert.sincProductSchwartz_deriv_le line 179

Source documentation

The extra derivative cost is precisely the sum of mask slopes.

theorem sincProductSchwartz_deriv_le (f : SchwartzMap ℝ ℂ)
    (n : ℕ) (a b c d x : ℝ) :
    ‖deriv (sincProductSchwartz f n a b c d) x‖ ≤
      ‖deriv f x‖+(2*(n:ℝ)*(|a|+|c|))*‖f x‖ := by
…

Mentions: OAI.LipschitzHilbert.sincProductSchwartz