L² compactness criterion: Fréchet–Kolmogorov (Euclidean, compact support case)

This file packages the final “precompactness via smoothing” step behind the Euclidean L² compactness criterion used by the Rellich–Kondrachov stack:

• the smoothing operator smoothL2 ψ has compact image on Metric.closedBall 0 R;
• the approximation inequality bounds ‖smoothL2 ψ u - extendByZeroL2 u‖ by a translation error.

We state the criterion at the level needed by the project: families of L² functions with common compact support (modeled as Lp ℝ 2 (volume.restrict K) and embedded into L²(volume) via extendByZeroL2).

Main results

• norm_smoothL2_sub_extendByZeroL2_le_of_integral_translateL2_sub_extendByZeroL2_le: if the translation error averaged against kernelMeasure ψ is ≤ η², then smoothing approximates extendByZeroL2 within η.
• totallyBounded_extendByZeroL2_image_of_forall_exists_translationIntegral_small: if a bounded family admits, at every scale ε, a kernel ψ for which the above translation error is uniformly small, then the embedded family is totally bounded in L²(volume).
• isCompact_closure_extendByZeroL2_image_of_forall_exists_translationIntegral_small: the corresponding compact-closure statement.

Tracking: Beads lean-103.5.2.26.5.3.2.2.3.

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

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

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

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.norm_smoothL2_sub_extendByZeroL2_le_of_integral_translateL2_sub_extendByZeroL2_le {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 ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (hψint : ∫ (x : E), ψ x = 1) {η : ℝ} (hη : 0 ≤ η) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) (htrans : ∫ (t : E), ‖(translateL2 MeasureTheory.volume (-t)) (extendByZeroL2 hKm u) - extendByZeroL2 hKm u‖ ^ 2 ∂kernelMeasure ψ ≤ η ^ 2) : ‖smoothL2 ψ hK hKm hψc hψcs u - extendByZeroL2 hKm u‖ ≤ η

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.totallyBounded_extendByZeroL2_image_of_forall_exists_translationIntegral_small {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hKm : MeasurableSet K) {R : ℝ} (hR : 0 ≤ R) {A : Set ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))} (hA : A ⊆ Metric.closedBall 0 R) (hApprox : ∀ (ε : ℝ), 0 < ε → ∃ (ψ : E → ℝ), Continuous ψ ∧ HasCompactSupport ψ ∧ (∀ (x : E), 0 ≤ ψ x) ∧ ∫ (x : E), ψ x = 1 ∧ ∀ u ∈ A, ∫ (t : E), ‖(translateL2 MeasureTheory.volume (-t)) (extendByZeroL2 hKm u) - extendByZeroL2 hKm u‖ ^ 2 ∂kernelMeasure ψ ≤ (ε / 2) ^ 2) : TotallyBounded (extendByZeroL2 hKm '' A)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.isCompact_closure_extendByZeroL2_image_of_forall_exists_translationIntegral_small {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hKm : MeasurableSet K) {R : ℝ} (hR : 0 ≤ R) {A : Set ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))} (hA : A ⊆ Metric.closedBall 0 R) (hApprox : ∀ (ε : ℝ), 0 < ε → ∃ (ψ : E → ℝ), Continuous ψ ∧ HasCompactSupport ψ ∧ (∀ (x : E), 0 ≤ ψ x) ∧ ∫ (x : E), ψ x = 1 ∧ ∀ u ∈ A, ∫ (t : E), ‖(translateL2 MeasureTheory.volume (-t)) (extendByZeroL2 hKm u) - extendByZeroL2 hKm u‖ ^ 2 ∂kernelMeasure ψ ≤ (ε / 2) ^ 2) : IsCompact (closure (extendByZeroL2 hKm '' A))