L² compactness criterion: transfer from BCF compactness to L² (Euclidean) #
This file transfers the Arzelà–Ascoli compactness of the BoundedContinuousFunction packaging of
smoothFun on the compact set K + tsupport ψ to a compactness statement in L²(volume).
Main results #
smoothL2_image_closedBall_isCompact: For a compact setKand a continuous compactly supported kernelψ, the family{ smoothL2 ψ u | ‖u‖ ≤ R }has compact closure inL²(volume).
Tracking: Beads lean-103.5.2.26.5.3.2.2.1.2.
@[implicit_reducible]
def
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableSpaceEL2CompactnessTransfer
{E : Type u_1}
[NormedAddCommGroup E]
:
Borel σ-algebra on the model space E.
Equations
Instances For
theorem
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothL2_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 (smoothL2 ψ hK hKm hψc hψcs '' Metric.closedBall 0 R))