L² compactness criterion: compact smoothing operator (Euclidean)

This file proves the compactness of the fixed-kernel smoothing operator used in the Fréchet–Kolmogorov / Riesz–Kolmogorov approach to Euclidean Rellich–Kondrachov.

Main results

• Kψ: the compact set K + tsupport ψ controlling supports of smoothed functions.
• smoothBCF: smoothFun packaged as a BoundedContinuousFunction on Kψ.
• uniformContinuous_ψ: UniformContinuous ψ from Continuous ψ + HasCompactSupport ψ.

The Arzelà–Ascoli compactness statement for smoothBCF lives in RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.ArzelaAscoli.

This is tracked under Beads lean-103.5.2.26.5.3.2.2.1.

@[instance_reducible]

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableSpaceEL2CompactnessCompactness {E : Type u_1} [NormedAddCommGroup E] : MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableSpaceEL2CompactnessCompactness = borel E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instBorelSpaceEL2CompactnessCompactness {E : Type u_1} [NormedAddCommGroup E] : BorelSpace E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instOpensMeasurableSpaceEL2CompactnessCompactness {E : Type u_1} [NormedAddCommGroup E] : OpensMeasurableSpace E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableAddEL2CompactnessCompactness {E : Type u_1} [NormedAddCommGroup E] : MeasurableAdd E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.instMeasurableNegEL2CompactnessCompactness {E : Type u_1} [NormedAddCommGroup E] : MeasurableNeg E

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Kψ {E : Type u_1} [NormedAddCommGroup E] {K : Set E} {ψ : E → ℝ} : Set E

The natural compact codomain for smoothing on K by a compactly supported kernel ψ.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.Kψ = K + tsupport ψ

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.isCompact_Kψ {E : Type u_1} [NormedAddCommGroup E] {K : Set E} {ψ : E → ℝ} (hK : IsCompact K) (hψcs : HasCompactSupport ψ) : IsCompact Kψ

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {ψ : E → ℝ} (hKm : MeasurableSet K) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : C(↑Kψ, ℝ)

Restrict the smoothed function to its compact domain as a continuous map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothBCF {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 ψ) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : BoundedContinuousFunction ↑Kψ ℝ

smoothFun packaged as a BoundedContinuousFunction on the compact set K + tsupport ψ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothBCF_apply {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 ψ) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) (x : ↑Kψ) : (smoothBCF hK hKm hψc hψcs u) x = smoothFun ψ u ↑x

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.uniformContinuous_ψ {E : Type u_1} [NormedAddCommGroup E] {ψ : E → ℝ} (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) : UniformContinuous ψ

The remainder of the compactness proof (Arzelà–Ascoli on the family smoothBCF '' closedBall) is tracked as part of lean-103.5.2.26.5.3.2.2.1.

We intentionally keep the helper lemmas above in this file so the final proof can stay short and only reference re-usable bounds.