SourceReproduction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual Schwartz reproducing kernels for the long-tree frequency rectangles. A smooth compact-frequency cutoff is constructed, rather than adding a reproduction hypothesis to the tree estimate.

theorem OAI.LipschitzHilbert.exists_schwartz_reproducing_kernel line 18
Source documentation
A smooth frequency cutoff equal to one throughout the prescribed closed interval. Its inverse transform is a Schwartz reproducing kernel.
```
theorem exists_schwartz_reproducing_kernel (R : ℝ) (hR : 0<R) :
    ∃ K : SchwartzMap ℝ ℂ, ∀ ξ, |ξ|≤R → 𝓕 K ξ=1 := by
…
```

theorem OAI.LipschitzHilbert.schwartz_convolution_reproduction line 32

Source documentation

Exact convolution reproduction from the original Fourier support.

theorem schwartz_convolution_reproduction (K f : SchwartzMap ℝ ℂ)
    (hK : ∀ ξ, 𝓕 f ξ≠0 → 𝓕 K ξ=1) :
    SchwartzMap.convolution (ContinuousLinearMap.mul ℂ ℂ) K f=f := by
…

theorem OAI.LipschitzHilbert.schwartz_integral_reproduction line 46
def OAI.LipschitzHilbert.scaledReproducingKernel line 56
Source documentation
The normalized spatial dilation has the correct scale and mass factor for frequency cutoffs at scale 1/r.
```
def scaledReproducingKernel (K : SchwartzMap ℝ ℂ) (r : ℝ) (hr : 0<r) :
    SchwartzMap ℝ ℂ := r⁻¹ • schwartzDilation K r⁻¹ (inv_ne_zero hr.ne')
```
Mentions: OAI.LipschitzHilbert.schwartzDilation
theorem OAI.LipschitzHilbert.scaledReproducingKernel_apply line 59
theorem OAI.LipschitzHilbert.scaledReproducingKernel_fourier line 66
theorem OAI.LipschitzHilbert.scaledReproducingKernel_envelope line 77
Source documentation
Every fixed Schwartz seminorm gives the scale-invariant polynomial kernel tail used in the cell-supremum estimate.
```
theorem scaledReproducingKernel_envelope (K : SchwartzMap ℝ ℂ)
    (r : ℝ) (hr : 0<r) (n : ℕ) (x : ℝ) :
    ‖scaledReproducingKernel K r hr x‖≤
      (schwartzEnvelopeConstant K n/r)*lineEnvelope 0 r n x := by
…
```
Mentions: OAI.LipschitzHilbert.scaledReproducingKernel, OAI.LipschitzHilbert.schwartzEnvelopeConstant, OAI.LipschitzHilbert.lineEnvelope
theorem OAI.LipschitzHilbert.scaledReproducingKernel_reproduction line 89