L² compactness criterion: Arzelà–Ascoli for the smoothing operator (Euclidean) #
This file proves the Arzelà–Ascoli step for the compact smoothing operator used in the Fréchet–Kolmogorov / Riesz–Kolmogorov approach to Euclidean Rellich–Kondrachov.
Main result #
smoothBCF_image_closedBall_isCompact: For a compact setKand a continuous compactly supported kernelψ, the family{ smoothFun ψ u | ‖u‖ ≤ R }restricted to the compact setK + tsupport ψhas compact closure inBoundedContinuousFunction.
Tracking: Beads lean-103.5.2.26.5.3.2.2.1.1.
@[implicit_reducible]
def
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableSpaceEL2CompactnessArzelaAscoli
{E : Type u_1}
[NormedAddCommGroup E]
:
Borel σ-algebra on the model space E.
Equations
Instances For
theorem
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothBCF_image_closedBall_isCompact
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{K : Set E}
{ψ : E → ℝ}
(hK : IsCompact K)
(hKm : MeasurableSet K)
(hψc : Continuous ψ)
(hψcs : HasCompactSupport ψ)
{R : ℝ}
(hR : 0 ≤ R)
:
IsCompact (closure (smoothBCF hK hKm hψc hψcs '' Metric.closedBall 0 R))