Lp Extension

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

def CKN.Foundation.Euclidean.lpInterL2Submodule (p : ENNReal) : Submodule ℝ ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume)

Submodule of Lᵖ classes whose representatives also belong to L².

Equations

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

structure CKN.Foundation.Euclidean.LpExtensionInput (p : ENNReal) (C : ℝ) : Type

Representative-level operator data sufficient to construct a bounded continuous Lᵖ extension.

• T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ

  Operator on scalar representatives to be extended from the Lᵖ–L² intersection.

• measurable {f : Parabolic.Vec3 → ℝ} : MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (self.T f)
• output_mem {f : Parabolic.Vec3 → ℝ} : MeasureTheory.MemLp f p MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.MemLp (self.T f) p MeasureTheory.volume
• congr_ae {f g : Parabolic.Vec3 → ℝ} : MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.MemLp g 2 MeasureTheory.volume → f =ᵐ[MeasureTheory.volume] g → self.T f =ᵐ[MeasureTheory.volume] self.T g
• add_ae {f g : Parabolic.Vec3 → ℝ} : MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.MemLp g 2 MeasureTheory.volume → self.T (f + g) =ᵐ[MeasureTheory.volume] self.T f + self.T g
• smul_ae (c : ℝ) {f : Parabolic.Vec3 → ℝ} : MeasureTheory.MemLp f 2 MeasureTheory.volume → self.T (c • f) =ᵐ[MeasureTheory.volume] c • self.T f
• bound {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp (self.T f) ⋯‖ ≤ C * ‖MeasureTheory.MemLp.toLp f hf‖

noncomputable def CKN.Foundation.Euclidean.lpInterL2Map {p : ENNReal} {C : ℝ} (h : LpExtensionInput p C) : ↥(lpInterL2Submodule p) →ₗ[ℝ] ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume)

Linear operator on the dense Lᵖ–L² intersection induced by the extension data.

Equations

• CKN.Foundation.Euclidean.lpInterL2Map h = { toFun := fun (u : ↥(CKN.Foundation.Euclidean.lpInterL2Submodule p)) => MeasureTheory.MemLp.toLp (h.T ↑↑↑u) ⋯, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def CKN.Foundation.Euclidean.lpExtensionCore {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) : ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume)

Continuous extension of the bounded operator from the dense Lᵖ–L² intersection.

Equations

• CKN.Foundation.Euclidean.lpExtensionCore hp h = (↑((CKN.Foundation.Euclidean.lpInterL2Map h).extendOfNorm (CKN.Foundation.Euclidean.lpInterL2Submodule p).subtype)).mkContinuous C ⋯

theorem CKN.Foundation.Euclidean.lpExtensionCore_agrees {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) (u : ↥(lpInterL2Submodule p)) : (lpExtensionCore hp h) ↑u = (lpInterL2Map h) u

theorem CKN.Foundation.Euclidean.lpExtensionCore_norm_le {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) (u : ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume)) : ‖(lpExtensionCore hp h) u‖ ≤ C * ‖u‖

noncomputable def CKN.Foundation.Euclidean.lpExtensionRepresentative {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) (f : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ℝ

Measurable representative of the extended operator, defined as zero outside its Lᵖ domain.

Equations

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

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_measurable {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : Measurable (lpExtensionRepresentative hp h f)

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_ae_eq_core {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : lpExtensionRepresentative hp h f =ᵐ[MeasureTheory.volume] ↑↑((lpExtensionCore hp h) (MeasureTheory.MemLp.toLp f hf))

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_memLp {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : MeasureTheory.MemLp (lpExtensionRepresentative hp h f) p MeasureTheory.volume

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_toLp_eq_core {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : MeasureTheory.MemLp.toLp (lpExtensionRepresentative hp h f) ⋯ = (lpExtensionCore hp h) (MeasureTheory.MemLp.toLp f hf)

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_norm_le {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp (lpExtensionRepresentative hp h f) ⋯‖ ≤ C * ‖MeasureTheory.MemLp.toLp f hf‖

noncomputable def CKN.Foundation.Euclidean.lpExtensionOperator {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) (f : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ℝ

Pointwise presentation of the continuous Lᵖ extension.

Equations

• CKN.Foundation.Euclidean.lpExtensionOperator hp h f = CKN.Foundation.Euclidean.lpExtensionRepresentative hp h f

theorem CKN.Foundation.Euclidean.lpExtensionOperator_memLp {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : MeasureTheory.MemLp (lpExtensionOperator hp h f) p MeasureTheory.volume

theorem CKN.Foundation.Euclidean.lpExtensionOperator_toLp_bound {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp (lpExtensionOperator hp h f) ⋯‖ ≤ C * ‖MeasureTheory.MemLp.toLp f hf‖

noncomputable def CKN.Foundation.Euclidean.lpExtensionTensorOperator {p : ENNReal} [Fact (1 ≤ p)] {C : Fin 3 → Fin 3 → ℝ} (hp : p ≠ ⊤) (h : (i j : Fin 3) → LpExtensionInput p (C i j)) (G : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ℝ

Sum of the componentwise extended operators acting on a tensor source.

Equations

• CKN.Foundation.Euclidean.lpExtensionTensorOperator hp h G x = ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Euclidean.lpExtensionOperator hp (h i j) (G i j) x

theorem CKN.Foundation.Euclidean.lpExtensionTensorOperator_memLp {p : ENNReal} [Fact (1 ≤ p)] {C : Fin 3 → Fin 3 → ℝ} (hp : p ≠ ⊤) (h : (i j : Fin 3) → LpExtensionInput p (C i j)) {G : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) p MeasureTheory.volume) : MeasureTheory.MemLp (lpExtensionTensorOperator hp h G) p MeasureTheory.volume

theorem CKN.Foundation.Euclidean.lpExtensionTensorOperator_eLpNorm_le {p : ENNReal} [Fact (1 ≤ p)] {C : Fin 3 → Fin 3 → ℝ} (hp : p ≠ ⊤) (h : (i j : Fin 3) → LpExtensionInput p (C i j)) (hC : ∀ (i j : Fin 3), 0 ≤ C i j) {G : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) p MeasureTheory.volume) : (∀ (i j : Fin 3), HasCompactSupport (G i j)) → ∀ (hpone : 1 ≤ p), MeasureTheory.eLpNorm (lpExtensionTensorOperator hp h G) p MeasureTheory.volume ≤ ∑ i : Fin 3, ∑ j : Fin 3, ENNReal.ofReal (C i j) * MeasureTheory.eLpNorm (G i j) p MeasureTheory.volume

noncomputable def CKN.Foundation.Euclidean.lpInterL2Input {p : ENNReal} {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ↥(lpInterL2Submodule p)

View a function belonging to both Lᵖ and L² as an element of the intersection submodule.

Equations

• CKN.Foundation.Euclidean.lpInterL2Input hf hf₂ = ⟨MeasureTheory.MemLp.toLp f hf, ⋯⟩

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_ae_eq_T {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) : lpExtensionRepresentative hp h f =ᵐ[MeasureTheory.volume] h.T f

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_add_ae {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f g : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) : lpExtensionRepresentative hp h (f + g) =ᵐ[MeasureTheory.volume] lpExtensionRepresentative hp h f + lpExtensionRepresentative hp h g

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_smul_ae {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) (c : ℝ) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : lpExtensionRepresentative hp h (c • f) =ᵐ[MeasureTheory.volume] c • lpExtensionRepresentative hp h f

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_congr_ae {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f g : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (hfg : f =ᵐ[MeasureTheory.volume] g) : lpExtensionRepresentative hp h f =ᵐ[MeasureTheory.volume] lpExtensionRepresentative hp h g

noncomputable def CKN.Foundation.Euclidean.lpPairingWith {p q : ENNReal} [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] (g : ↥(MeasureTheory.Lp ℝ q MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume) →L[ℝ] ℝ

Continuous linear pairing against a fixed function in the conjugate Lᵖ space.

Equations

• CKN.Foundation.Euclidean.lpPairingWith g = (ContinuousLinearMap.apply ℝ ℝ) g ∘SL ContinuousLinearMap.lpPairing MeasureTheory.volume p q (ContinuousLinearMap.mul ℝ ℝ)

theorem CKN.Foundation.Euclidean.lpExtension_distribution_identity_transfer {p q : ENNReal} [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {lap rhs : Parabolic.Vec3 → ℝ} (hlap : MeasureTheory.MemLp lap q MeasureTheory.volume) (hrhs : MeasureTheory.MemLp rhs q MeasureTheory.volume) (s : Set ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume)) (hs : Dense s) : (∀ u ∈ s, HasCompactSupport ↑↑u) → ∀ (hs₂ : ∀ u ∈ s, MeasureTheory.MemLp (↑↑u) 2 MeasureTheory.volume) (hidentity : ∀ u ∈ s, ∫ (x : Parabolic.Vec3), h.T (↑↑u) x * lap x = ∫ (x : Parabolic.Vec3), ↑↑u x * rhs x) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume), HasCompactSupport f → ∫ (x : Parabolic.Vec3), lpExtensionRepresentative hp h f x * lap x = ∫ (x : Parabolic.Vec3), f x * rhs x

theorem CKN.Foundation.Euclidean.lpExtensionTensorOperator_distributional_pairing {p q : ENNReal} [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] {C : Fin 3 → Fin 3 → ℝ} (hp : p ≠ ⊤) (h : (i j : Fin 3) → LpExtensionInput p (C i j)) {lap : Parabolic.Vec3 → ℝ} (hlap : MeasureTheory.MemLp lap q MeasureTheory.volume) {rhs : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ} (hrhs : ∀ (i j : Fin 3), MeasureTheory.MemLp (rhs i j) q MeasureTheory.volume) (s : Set ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume)) (hs : Dense s) (hs_compact : ∀ u ∈ s, HasCompactSupport ↑↑u) (hs₂ : ∀ u ∈ s, MeasureTheory.MemLp (↑↑u) 2 MeasureTheory.volume) (hidentity : ∀ (i j : Fin 3), ∀ u ∈ s, ∫ (x : Parabolic.Vec3), (h i j).T (↑↑u) x * lap x = ∫ (x : Parabolic.Vec3), ↑↑u x * rhs i j x) {G : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) p MeasureTheory.volume) (hGc : ∀ (i j : Fin 3), HasCompactSupport (G i j)) : ∫ (x : Parabolic.Vec3), lpExtensionTensorOperator hp h G x * lap x = ∫ (x : Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * rhs i j x

theorem CKN.Foundation.Euclidean.lpExtensionTensorOperator_agrees_exterior {p : ENNReal} [Fact (1 ≤ p)] {C : Fin 3 → Fin 3 → ℝ} (hp : p ≠ ⊤) (h : (i j : Fin 3) → LpExtensionInput p (C i j)) {G : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ} {L : Fin 3 → Fin 3 → (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} (hExterior : ∀ (i j : Fin 3), ∀ x ∉ tsupport (G i j), lpExtensionOperator hp (h i j) (G i j) x = L i j (G i j) x) (x : Parabolic.Vec3) : (∀ (i j : Fin 3), x ∉ tsupport (G i j)) → lpExtensionTensorOperator hp h G x = ∑ i : Fin 3, ∑ j : Fin 3, L i j (G i j) x

theorem CKN.Foundation.Euclidean.lpExtensionRepresentative_bound {p : ENNReal} [Fact (1 ≤ p)] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ‖(lpExtensionCore hp h) (MeasureTheory.MemLp.toLp f hf)‖ ≤ C * ‖MeasureTheory.MemLp.toLp f hf‖