L² compactness criterion: smoothing setup (Euclidean)

This file provides the basic “extend by zero + smooth by convolution” infrastructure used in the Fréchet–Kolmogorov / Riesz–Kolmogorov approach to Euclidean Rellich–Kondrachov.

Main results

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.extendByZeroL2: extend u : L²(volume.restrict K) by zero to an element of L²(volume).
• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothL2: a smoothing operator obtained by convolution with a compactly supported continuous kernel ψ.

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

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

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

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

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.extendByZeroFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : E → ℝ

Extend an L² function on K by zero to a pointwise function on the ambient space.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.extendByZeroFun u = K.indicator fun (x : E) => ↑↑u x

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.hasCompactSupport_extendByZeroFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : HasCompactSupport (extendByZeroFun u)

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.extendByZeroL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hKm : MeasurableSet K) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

extendByZeroFun packaged as an element of L²(volume).

Equations

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

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.extendByZeroL2_ae_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hKm : MeasurableSet K) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : ↑↑(extendByZeroL2 hKm u) =ᵐ[MeasureTheory.volume] extendByZeroFun u

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.extendByZeroL2_eq_extendByZeroₗᵢ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hKm : MeasurableSet K) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : extendByZeroL2 hKm u = (MeasureTheory.Lp.extendByZeroₗᵢ hKm) u

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.norm_extendByZeroL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hKm : MeasurableSet K) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : ‖extendByZeroL2 hKm u‖ = ‖u‖

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (ψ : E → ℝ) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : E → ℝ

Smoothing by convolution with a fixed kernel ψ, applied to the zero-extension from K.

Equations

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

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.continuous_smoothFun {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))) : Continuous (smoothFun ψ u)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.hasCompactSupport_smoothFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (ψ : E → ℝ) (hK : IsCompact K) (hψcs : HasCompactSupport ψ) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : HasCompactSupport (smoothFun ψ u)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.support_smoothFun_subset_add_tsupport {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (ψ : E → ℝ) (u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict K))) : Function.support (smoothFun ψ u) ⊆ K + tsupport ψ

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothL2 {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))) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

smoothFun packaged as an element of L²(volume).

Equations

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

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2Compactness.smoothL2_ae_eq {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))) : ↑↑(smoothL2 ψ hK hKm hψc hψcs u) =ᵐ[MeasureTheory.volume] smoothFun ψ u