Indexed pressure-extension identification #
The global pressure operator in this file is the indexed L^(3/2) extension.
The ordinary Newtonian kernel expression is an exterior tail object and is not
used by the global identification.
noncomputable def
CKN.pressureSecondExtensionOperator
(hL2 : (i j : Fin 3) → Foundation.Euclidean.RieszSecondL2Input i j)
(hWeak11 :
∀ (i j : Fin 3) (f : Foundation.Parabolic.Vec3 → ℝ),
Measurable f →
MeasureTheory.Integrable f MeasureTheory.volume →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
∀ (l : ℝ),
0 < l →
MeasureTheory.volume
{x : Foundation.Parabolic.Vec3 | l < |Foundation.Euclidean.rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal Foundation.Euclidean.rieszSecondWeakTypeConstant * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
(G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ)
:
Pressure reconstruction operator from the continuous second-Riesz tensor extension.
Equations
- CKN.pressureSecondExtensionOperator hL2 hWeak11 G = CKN.Foundation.Euclidean.rieszSecondP1ExtensionTensorOperator hL2 hWeak11 G
Instances For
theorem
CKN.pressureSecondExtension_memLp
(hL2 : (i j : Fin 3) → Foundation.Euclidean.RieszSecondL2Input i j)
(hWeak11 :
∀ (i j : Fin 3) (f : Foundation.Parabolic.Vec3 → ℝ),
Measurable f →
MeasureTheory.Integrable f MeasureTheory.volume →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
∀ (l : ℝ),
0 < l →
MeasureTheory.volume
{x : Foundation.Parabolic.Vec3 | l < |Foundation.Euclidean.rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal Foundation.Euclidean.rieszSecondWeakTypeConstant * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
{G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
:
MeasureTheory.MemLp (pressureSecondExtensionOperator hL2 hWeak11 G) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume
theorem
CKN.pressureSecondExtension_distributional_identity
(hL2 : (i j : Fin 3) → Foundation.Euclidean.RieszSecondL2Input i j)
(hWeak11 :
∀ (i j : Fin 3) (f : Foundation.Parabolic.Vec3 → ℝ),
Measurable f →
MeasureTheory.Integrable f MeasureTheory.volume →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
∀ (l : ℝ),
0 < l →
MeasureTheory.volume
{x : Foundation.Parabolic.Vec3 | l < |Foundation.Euclidean.rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal Foundation.Euclidean.rieszSecondWeakTypeConstant * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
{G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
{ψ : Foundation.Parabolic.Vec3 → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
:
∫ (x : Foundation.Parabolic.Vec3), pressureSecondExtensionOperator hL2 hWeak11 G x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * mixedSecond ψ i j x
theorem
CKN.pressureP1_hident_of_indexed_extension
{p₁ : Foundation.Parabolic.Vec3 → ℝ}
{G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
{T : Fin 3 → Fin 3 → (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ}
{C : ℝ}
(hC : 0 ≤ C)
(hP1 :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x)
MeasureTheory.volume →
∫ (x : Foundation.Parabolic.Vec3), p₁ x * spatialLaplacian ψ x = pressureSecondPairing G ψ)
(hDeltaT :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
(fun (y : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) y) x * spatialLaplacian ψ x)
MeasureTheory.volume →
∫ (x : Foundation.Parabolic.Vec3), (fun (y : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) y) x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * mixedSecond ψ i j x)
(hP1Int :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hTInt :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
(fun (y : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) y) x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hmem :
∀ (ρ : ℝ),
0 < ρ →
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
p₁ x - (fun (y : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) y) x)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)))
(hgrowth :
∀ (ρ : ℝ),
0 < ρ →
MeasureTheory.lpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
p₁ x - (fun (y : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) y) x)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ))
:
p₁ =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) x
theorem
CKN.pressureP1_hident_of_pressureSecondExtension
(hL2 : (i j : Fin 3) → Foundation.Euclidean.RieszSecondL2Input i j)
(hWeak11 :
∀ (i j : Fin 3) (f : Foundation.Parabolic.Vec3 → ℝ),
Measurable f →
MeasureTheory.Integrable f MeasureTheory.volume →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
∀ (l : ℝ),
0 < l →
MeasureTheory.volume
{x : Foundation.Parabolic.Vec3 | l < |Foundation.Euclidean.rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal Foundation.Euclidean.rieszSecondWeakTypeConstant * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
{p₁ : Foundation.Parabolic.Vec3 → ℝ}
{G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
{C : ℝ}
(hC : 0 ≤ C)
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(hP1 :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x)
MeasureTheory.volume →
∫ (x : Foundation.Parabolic.Vec3), p₁ x * spatialLaplacian ψ x = pressureSecondPairing G ψ)
(hP1Int :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hTInt :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
pressureSecondExtensionOperator hL2 hWeak11 G x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hmem :
∀ (ρ : ℝ),
0 < ρ →
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) => p₁ x - pressureSecondExtensionOperator hL2 hWeak11 G x)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)))
(hgrowth :
∀ (ρ : ℝ),
0 < ρ →
MeasureTheory.lpNorm
(fun (x : Foundation.Parabolic.Vec3) => p₁ x - pressureSecondExtensionOperator hL2 hWeak11 G x)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ))
:
p₁ =ᵐ[MeasureTheory.volume] pressureSecondExtensionOperator hL2 hWeak11 G