KernelScaling.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Scaling a cutoff kernel

The normalization and weighted L¹ moment are preserved under T k(Tx). Thus a single Schwartz kernel gives a uniform family of interval approximations at all positive truncation heights.

def OAI.CubicFirstMoment.scaledKernel line 18
theorem OAI.CubicFirstMoment.integrable_scaledKernel line 20
theorem OAI.CubicFirstMoment.integral_scaledKernel line 24
theorem OAI.CubicFirstMoment.scaledKernel_moment_integrand line 31
theorem OAI.CubicFirstMoment.integrable_scaledKernel_moment line 39
theorem OAI.CubicFirstMoment.kernelMoment_scaledKernel line 46
theorem OAI.CubicFirstMoment.integrable_kernelMoment_schwartz line 55
Source documentation
Schwartz decay supplies the integrable moment needed by the cutoff, without imposing a quantitative tail estimate as a hypothesis.
```
theorem integrable_kernelMoment_schwartz (k : SchwartzMap ℝ ℂ) :
    Integrable (fun y => ‖k y‖ * (1 + |y|)^2) := by
…
```

theorem OAI.CubicFirstMoment.scaled_schwartz_interval_error line 68

Source documentation

Uniform endpoint estimate for the entire scaled Schwartz family.

theorem scaled_schwartz_interval_error (k : SchwartzMap ℝ ℂ)
    (hmass : ∫ y, k y = 1) {T : ℝ} (hT : 0 < T) (a b s : ℝ) :
    ‖(intervalStep a b s : ℂ) - intervalSmoothing (scaledKernel k T) a b s‖ ≤
      kernelMoment k 1 / (1 + T*|s-a|)^2 +
        kernelMoment k 1 / (1 + T*|s-b|)^2 := by
…

Mentions: OAI.CubicFirstMoment.intervalStep, OAI.CubicFirstMoment.intervalSmoothing, OAI.CubicFirstMoment.scaledKernel, OAI.CubicFirstMoment.kernelMoment