KernelTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative kernel tails

A finite weighted L¹ moment gives a uniform bound for the two endpoint tails. Scaling the kernel will make the moment independent of the truncation height, as required for a sharp cutoff.

def OAI.CubicFirstMoment.kernelMoment line 18
theorem OAI.CubicFirstMoment.kernel_tail_le_moment line 21

theorem OAI.CubicFirstMoment.intervalSmoothing_error_le_moment line 43

Source documentation

A moment bound proves the error estimate; it is not assumed as an unproved boundary approximation.

theorem intervalSmoothing_error_le_moment {k : ℝ → ℂ} (hk : Integrable k)
    (hmass : ∫ y, k y = 1) {T : ℝ} (hT : 0 ≤ T)
    (hM : Integrable (fun y => ‖k y‖ * (1 + T * |y|) ^ 2)) (a b s : ℝ) :
    ‖(intervalStep a b s : ℂ) - intervalSmoothing k a b s‖ ≤
      kernelMoment k T / (1 + T*|s-a|)^2 +
        kernelMoment k T / (1 + T*|s-b|)^2 :=
…

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