L² compactness criterion: approximation-by-translation bounds (Euclidean)

This file will prove the key inequality used in the Fréchet–Kolmogorov approach: smoothing by a probability kernel controls the L² error by the translation modulus.

Main results (planned)

The principal statement will control ‖smoothL2 ψ u - extendByZeroL2 u‖₂ by an average (or sup) of ‖translateL2 t (extendByZeroL2 u) - extendByZeroL2 u‖₂ over t in the support of ψ.

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

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

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

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.kernelMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (ψ : E → ℝ) : MeasureTheory.Measure E

The measure with density ψ with respect to Lebesgue measure. This will be a probability measure once ψ ≥ 0 and ∫ ψ = 1.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.kernelMeasure ψ = MeasureTheory.volume.withDensity fun (x : E) => ENNReal.ofReal (ψ x)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.kernelMeasure_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (ψ : E → ℝ) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (hψint : ∫ (x : E), ψ x = 1) : (kernelMeasure ψ) Set.univ = 1

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.isProbabilityMeasure_kernelMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (ψ : E → ℝ) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (hψint : ∫ (x : E), ψ x = 1) : MeasureTheory.IsProbabilityMeasure (kernelMeasure ψ)

The kernel measure kernelMeasure ψ is a probability measure when ψ is a continuous, compactly supported, nonnegative density integrating to 1.

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.integral_kernelMeasure_eq_integral_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (ψ : E → ℝ) (hψc : Continuous ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (g : E → ℝ) : ∫ (x : E), g x ∂kernelMeasure ψ = ∫ (x : E), ψ x • g x

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.integral_kernelMeasure_eq_integral_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (ψ : E → ℝ) (hψc : Continuous ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (g : E → ℝ) : ∫ (x : E), g x ∂kernelMeasure ψ = ∫ (x : E), ψ x * g x

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothFun_eq_integral_kernelMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (ψ : E → ℝ) (hψc : Continuous ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) (x : E) : smoothFun ψ u x = ∫ (t : E), extendByZeroFun u (x - t) ∂kernelMeasure ψ

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.sq_integral_le_integral_sq_of_isProbabilityMeasure {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (f : α → ℝ) (hf : MeasureTheory.MemLp f 2 μ) : (∫ (x : α), f x ∂μ) ^ 2 ≤ ∫ (x : α), f x ^ 2 ∂μ

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.norm_sq_translateL2_sub_extendByZeroL2_eq_integral_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hKm : MeasurableSet K) (t : E) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : ‖(translateL2 MeasureTheory.volume (-t)) (extendByZeroL2 hKm u) - extendByZeroL2 hKm u‖ ^ 2 = ∫ (x : E), (extendByZeroFun u (x - t) - extendByZeroFun u x) ^ 2

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothFun_sub_extendByZeroFun_sq_le_integral_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (ψ : E → ℝ) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (hψint : ∫ (x : E), ψ x = 1) (hKm : MeasurableSet K) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) (x : E) : (smoothFun ψ u x - extendByZeroFun u x) ^ 2 ≤ ∫ (t : E), (extendByZeroFun u (x - t) - extendByZeroFun u x) ^ 2 ∂kernelMeasure ψ

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.norm_sq_smoothL2_sub_extendByZeroL2_le_integral_norm_sq_translateL2_sub_extendByZeroL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hKm : MeasurableSet K) (ψ : E → ℝ) (hψc : Continuous ψ) (hψcs : HasCompactSupport ψ) (hψ0 : ∀ (x : E), 0 ≤ ψ x) (hψint : ∫ (x : E), ψ x = 1) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : ‖smoothL2 ψ hK hKm hψc hψcs u - extendByZeroL2 hKm u‖ ^ 2 ≤ ∫ (t : E), ‖(translateL2 MeasureTheory.volume (-t)) (extendByZeroL2 hKm u) - extendByZeroL2 hKm u‖ ^ 2 ∂kernelMeasure ψ