L² compactness criterion: existence of small-support probability kernels (Euclidean) #
This file provides a “kernel factory” for the Euclidean Fréchet–Kolmogorov / Riesz–Kolmogorov
criterion: for any radius δ > 0, produce a continuous compactly supported function ψ : E → ℝ
such that:
ψ ≥ 0,tsupport ψ ⊆ Metric.ball 0 δ,∫ ψ = 1(sokernelMeasure ψis a probability measure).
The construction uses mathlib’s exists_smooth_tsupport_subset bump-function lemma and normalizes
by its (positive) integral.
Tracking: Beads lean-103.5.2.26.5.3.2.2.5.
@[implicit_reducible]
def
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableSpaceEL2CompactnessKernels
{E : Type u_1}
[NormedAddCommGroup E]
:
Borel σ-algebra on the model space E.
Equations
Instances For
theorem
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.exists_kernel_tsupport_subset_ball_integral_eq_one
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{δ : ℝ}
(hδ : 0 < δ)
:
∃ (ψ : E → ℝ),
Continuous ψ ∧ HasCompactSupport ψ ∧ (∀ (x : E), 0 ≤ ψ x) ∧ ∫ (x : E), ψ x = 1 ∧ tsupport ψ ⊆ Metric.ball 0 δ
For any δ > 0, there exists a continuous compactly supported kernel ψ supported in
Metric.ball 0 δ, with ψ ≥ 0 and ∫ ψ = 1 (w.r.t. Lebesgue measure).