The pressure-difference functional on Schwartz tests

The coefficients of the velocity terms belong to ordinary L², and the tensor coefficients belong to L¹. All pairings below are actual Lebesgue integrals. The final functional uses the spatial Laplacian and coordinate derivatives from the equation, and the double Riesz test operator.

Fourier bounds for pressure test functionals

theorem NavierStokesR3.PressureTestBounds.integrable_inverse_weight_sq : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2)⁻¹ ^ 2) MeasureTheory.volume

The dimension-three integrable weight used in the Fourier Cauchy--Schwarz bound.

noncomputable def NavierStokesR3.PressureTestBounds.fourierMomentConstant : ℝ

A finite numerical constant depending only on three-dimensional Lebesgue measure.

Equations

• NavierStokesR3.PressureTestBounds.fourierMomentConstant = √(∫ (ξ : NavierStokesR3.ProblemStatement.Space), (1 + ‖ξ‖ ^ 2)⁻¹ ^ 2)

theorem NavierStokesR3.PressureTestBounds.fourierMomentConstant_nonneg : 0 ≤ fourierMomentConstant

theorem NavierStokesR3.PressureTestBounds.integral_first_moment_le {f : ProblemStatement.Space → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hw : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖f ξ‖ ^ 2) MeasureTheory.volume) : ∫ (ξ : ProblemStatement.Space), ‖ξ‖ * ‖f ξ‖ ≤ fourierMomentConstant * √(∫ (ξ : ProblemStatement.Space), (1 + ‖ξ‖ ^ 2) ^ 3 * ‖f ξ‖ ^ 2)

The elementary weighted Cauchy--Schwarz estimate behind the H³ bounds.

theorem NavierStokesR3.PressureTestBounds.fourierHNormSq_nonneg (s : ℕ) (ψ : Comparison.ComplexTest) : 0 ≤ Comparison.fourierHNormSq s ψ

theorem NavierStokesR3.PressureTestBounds.sqrt_l2Sq_le_of_fourier_bound (ψ φ : Comparison.ComplexTest) {C : ℝ} (hC : 0 ≤ C) (hw : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume) (hφ : ∀ (ξ : ProblemStatement.Space), ‖(EulerSobolev.schwartzFourier φ) ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2) * ‖(EulerSobolev.schwartzFourier ψ) ξ‖) : √(Comparison.l2Sq ⇑φ) ≤ C * √(Comparison.fourierHNormSq 3 ψ)

A Fourier multiplier of order at most two has the required H³ control.

theorem NavierStokesR3.PressureTestBounds.norm_fourier_partialCLM (i : Fin 3) (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : ‖(EulerSobolev.schwartzFourier ((HarmonicTestFunctionals.partialCLM i) ψ)) ξ‖ = 2 * Real.pi * ‖ξ.ofLp i‖ * ‖(EulerSobolev.schwartzFourier ψ) ξ‖

Exact magnitude of the coordinate-derivative Fourier multiplier.

theorem NavierStokesR3.PressureTestBounds.norm_fourier_partialCLM_le (i : Fin 3) (ψ : Comparison.ComplexTest) (ξ : ProblemStatement.Space) : ‖(EulerSobolev.schwartzFourier ((HarmonicTestFunctionals.partialCLM i) ψ)) ξ‖ ≤ 2 * Real.pi * ‖ξ‖ * ‖(EulerSobolev.schwartzFourier ψ) ξ‖

theorem NavierStokesR3.PressureTestBounds.norm_test_le_integral_fourier (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : ‖ψ x‖ ≤ ∫ (ξ : ProblemStatement.Space), ‖(EulerSobolev.schwartzFourier ψ) ξ‖

theorem NavierStokesR3.PressureTestBounds.integral_norm_fourier_partialCLM_le_of_integrable (i : Fin 3) (ψ : Comparison.ComplexTest) (hw : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume) : ∫ (ξ : ProblemStatement.Space), ‖(EulerSobolev.schwartzFourier ((HarmonicTestFunctionals.partialCLM i) ψ)) ξ‖ ≤ 2 * Real.pi * fourierMomentConstant * √(Comparison.fourierHNormSq 3 ψ)

theorem NavierStokesR3.PressureTestBounds.sqrt_l2Sq_test_le_of_integrable (ψ : Comparison.ComplexTest) (hw : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume) : √(Comparison.l2Sq ⇑ψ) ≤ √(Comparison.fourierHNormSq 3 ψ)

theorem NavierStokesR3.PressureTestBounds.sqrt_l2Sq_partial_partial_le_of_integrable (i : Fin 3) (ψ : Comparison.ComplexTest) (hw : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume) : √(Comparison.l2Sq ⇑((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM i) ψ))) ≤ (2 * Real.pi) ^ 2 * √(Comparison.fourierHNormSq 3 ψ)

theorem NavierStokesR3.PressureTestBounds.norm_partialCLM_le_of_integrable (i : Fin 3) (ψ : Comparison.ComplexTest) (hw : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume) (x : ProblemStatement.Space) : ‖((HarmonicTestFunctionals.partialCLM i) ψ) x‖ ≤ 2 * Real.pi * fourierMomentConstant * √(Comparison.fourierHNormSq 3 ψ)

theorem NavierStokesR3.PressureTestBounds.norm_rieszTest_partialCLM_le_of_integrable (i j k : Fin 3) (ψ : Comparison.ComplexTest) (hw : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => (1 + ‖ξ‖ ^ 2) ^ 3 * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ^ 2) MeasureTheory.volume) (x : ProblemStatement.Space) : ‖Comparison.rieszTest i j ((HarmonicTestFunctionals.partialCLM k) ψ) x‖ ≤ 2 * Real.pi * fourierMomentConstant * √(Comparison.fourierHNormSq 3 ψ)

theorem NavierStokesR3.PressureTestBounds.fourier_first_moment_le (ψ : Comparison.ComplexTest) : ∫ (ξ : ProblemStatement.Space), ‖ξ‖ * ‖(EulerSobolev.schwartzFourier ψ) ξ‖ ≤ fourierMomentConstant * √(Comparison.fourierHNormSq 3 ψ)

The first moment of a Schwartz Fourier transform is controlled uniformly by H³.

theorem NavierStokesR3.PressureTestBounds.integral_norm_fourier_partialCLM_le (i : Fin 3) (ψ : Comparison.ComplexTest) : ∫ (ξ : ProblemStatement.Space), ‖(EulerSobolev.schwartzFourier ((HarmonicTestFunctionals.partialCLM i) ψ)) ξ‖ ≤ 2 * Real.pi * fourierMomentConstant * √(Comparison.fourierHNormSq 3 ψ)

theorem NavierStokesR3.PressureTestBounds.sqrt_l2Sq_test_le (ψ : Comparison.ComplexTest) : √(Comparison.l2Sq ⇑ψ) ≤ √(Comparison.fourierHNormSq 3 ψ)

The spatial L² norm of a test is at most its Fourier H³ norm.

theorem NavierStokesR3.PressureTestBounds.sqrt_l2Sq_partial_partial_le (i : Fin 3) (ψ : Comparison.ComplexTest) : √(Comparison.l2Sq ⇑((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM i) ψ))) ≤ (2 * Real.pi) ^ 2 * √(Comparison.fourierHNormSq 3 ψ)

Coordinate second derivatives have a common H³ bound.

theorem NavierStokesR3.PressureTestBounds.norm_partialCLM_le (i : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : ‖((HarmonicTestFunctionals.partialCLM i) ψ) x‖ ≤ 2 * Real.pi * fourierMomentConstant * √(Comparison.fourierHNormSq 3 ψ)

The first derivative is bounded pointwise by one constant times the Fourier H³ norm.

theorem NavierStokesR3.PressureTestBounds.norm_rieszTest_partialCLM_le (i j k : Fin 3) (ψ : Comparison.ComplexTest) (x : ProblemStatement.Space) : ‖Comparison.rieszTest i j ((HarmonicTestFunctionals.partialCLM k) ψ) x‖ ≤ 2 * Real.pi * fourierMomentConstant * √(Comparison.fourierHNormSq 3 ψ)

Applying the bounded Riesz symbol preserves the same pointwise test bound.

theorem NavierStokesR3.PressureTestBounds.exists_uniform_test_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ψ : Comparison.ComplexTest), √(Comparison.l2Sq ⇑ψ) ≤ C * √(Comparison.fourierHNormSq 3 ψ) ∧ (∀ (i : Fin 3), √(Comparison.l2Sq ⇑((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM i) ψ))) ≤ C * √(Comparison.fourierHNormSq 3 ψ)) ∧ (∀ (i : Fin 3) (x : ProblemStatement.Space), ‖((HarmonicTestFunctionals.partialCLM i) ψ) x‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)) ∧ ∀ (i j k : Fin 3) (x : ProblemStatement.Space), ‖Comparison.rieszTest i j ((HarmonicTestFunctionals.partialCLM k) ψ) x‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)

One constant controls all test expressions appearing in pressure recovery.

theorem NavierStokesR3.PressureFunctionals.integrable_l2_pair {W : ProblemStatement.Space → ℝ} (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) (ψ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(W x) * ψ x) MeasureTheory.volume

Pairing an L² coefficient with a Schwartz test is integrable.

theorem NavierStokesR3.PressureFunctionals.norm_l2_pair_le {W : ProblemStatement.Space → ℝ} (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) (ψ : Comparison.ComplexTest) : ‖∫ (x : ProblemStatement.Space), ↑(W x) * ψ x‖ ≤ √(Comparison.l2Sq W) * √(Comparison.l2Sq ⇑ψ)

Cauchy--Schwarz for the actual coefficient/test pairing.

theorem NavierStokesR3.PressureFunctionals.integrable_l1_pair {g : ProblemStatement.Space → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ψ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(g x) * ψ x) MeasureTheory.volume

An L¹ coefficient may be paired with any Schwartz test.

theorem NavierStokesR3.PressureFunctionals.integrable_l1_riesz_pair {g : ProblemStatement.Space → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (i j : Fin 3) (ψ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(g x) * Comparison.rieszTest i j ψ x) MeasureTheory.volume

The canonical pressure pairing is finite for an L¹ coefficient.

theorem NavierStokesR3.PressureFunctionals.norm_l1_pair_le_of_bound {g : ProblemStatement.Space → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) {f : ProblemStatement.Space → ℂ} (hf : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(g x) * f x) MeasureTheory.volume) {B : ℝ} (hB : ∀ (x : ProblemStatement.Space), ‖f x‖ ≤ B) : ‖∫ (x : ProblemStatement.Space), ↑(g x) * f x‖ ≤ (∫ (x : ProblemStatement.Space), ‖g x‖) * B

A pointwise test bound gives the usual L¹ pairing estimate.

noncomputable def NavierStokesR3.PressureFunctionals.testValueLinear : Comparison.ComplexTest →ₗ[ℂ] ProblemStatement.Space → ℂ

The ordinary inclusion of Schwartz tests into complex-valued functions.

Equations

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

noncomputable def NavierStokesR3.PressureFunctionals.integralPairLinear (g : ProblemStatement.Space → ℝ) (T : Comparison.ComplexTest →ₗ[ℂ] ProblemStatement.Space → ℂ) (hint : ∀ (ψ : Comparison.ComplexTest), MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(g x) * T ψ x) MeasureTheory.volume) : Comparison.ComplexTest →ₗ[ℂ] ℂ

Integrating a linear family of tests against a fixed coefficient is linear when every displayed integrand is integrable.

Equations

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

noncomputable def NavierStokesR3.PressureFunctionals.l2PairLinear (W : ProblemStatement.Space → ℝ) (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) : Comparison.ComplexTest →ₗ[ℂ] ℂ

The linear L² coefficient pairing.

Equations

• NavierStokesR3.PressureFunctionals.l2PairLinear W hW = NavierStokesR3.PressureFunctionals.integralPairLinear W NavierStokesR3.PressureFunctionals.testValueLinear ⋯

noncomputable def NavierStokesR3.PressureFunctionals.l1PairLinear (g : ProblemStatement.Space → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : Comparison.ComplexTest →ₗ[ℂ] ℂ

The linear L¹ coefficient pairing.

Equations

• NavierStokesR3.PressureFunctionals.l1PairLinear g hg = NavierStokesR3.PressureFunctionals.integralPairLinear g NavierStokesR3.PressureFunctionals.testValueLinear ⋯

@[simp]

theorem NavierStokesR3.PressureFunctionals.l2PairLinear_apply (W : ProblemStatement.Space → ℝ) (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) (ψ : Comparison.ComplexTest) : (l2PairLinear W hW) ψ = ∫ (x : ProblemStatement.Space), ↑(W x) * ψ x

@[simp]

theorem NavierStokesR3.PressureFunctionals.l1PairLinear_apply (g : ProblemStatement.Space → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ψ : Comparison.ComplexTest) : (l1PairLinear g hg) ψ = ∫ (x : ProblemStatement.Space), ↑(g x) * ψ x

noncomputable def NavierStokesR3.PressureFunctionals.averagedPressureDifferenceValue (W0 W1 : ProblemStatement.Space → ℝ) (G : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ) (k : Fin 3) (ψ : Comparison.ComplexTest) : ℂ

The coefficients are the two time averages of velocity and the time average of the quadratic tensor in the conservative pressure equation.

Equations

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

theorem NavierStokesR3.PressureFunctionals.integrable_terms {W0 W1 : ProblemStatement.Space → ℝ} {G : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ} (hW0 : MeasureTheory.MemLp W0 2 MeasureTheory.volume) (hW1 : MeasureTheory.MemLp W1 2 MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.Integrable (G i j) MeasureTheory.volume) (k : Fin 3) (ψ : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(W0 x) * (HarmonicTestFunctionals.laplacianCLM ψ) x) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(W1 x) * ψ x) MeasureTheory.volume ∧ (∀ (i : Fin 3), MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(G k i x) * ((HarmonicTestFunctionals.partialCLM i) ψ) x) MeasureTheory.volume) ∧ ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(G i j x) * Comparison.rieszTest i j ((HarmonicTestFunctionals.partialCLM k) ψ) x) MeasureTheory.volume

Every term of the pressure-difference functional is an integrable pairing.

theorem NavierStokesR3.PressureFunctionals.l2_pair_laplacian_eq_sum {W : ProblemStatement.Space → ℝ} (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) (ψ : Comparison.ComplexTest) : ∫ (x : ProblemStatement.Space), ↑(W x) * (HarmonicTestFunctionals.laplacianCLM ψ) x = ∑ i : Fin 3, ∫ (x : ProblemStatement.Space), ↑(W x) * ((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM i) ψ)) x

theorem NavierStokesR3.PressureFunctionals.norm_l2_laplacian_pair_le {W : ProblemStatement.Space → ℝ} (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) (ψ : Comparison.ComplexTest) {B : ℝ} (hB : ∀ (i : Fin 3), √(Comparison.l2Sq ⇑((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM i) ψ))) ≤ B) : ‖∫ (x : ProblemStatement.Space), ↑(W x) * (HarmonicTestFunctionals.laplacianCLM ψ) x‖ ≤ 3 * √(Comparison.l2Sq W) * B

theorem NavierStokesR3.PressureFunctionals.averagedPressureDifferenceValue_bound {W0 W1 : ProblemStatement.Space → ℝ} {G : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ} (hW0 : MeasureTheory.MemLp W0 2 MeasureTheory.volume) (hW1 : MeasureTheory.MemLp W1 2 MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.Integrable (G i j) MeasureTheory.volume) (k : Fin 3) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ψ : Comparison.ComplexTest), ‖averagedPressureDifferenceValue W0 W1 G k ψ‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)

The actual pressure-difference expression is bounded by the Fourier H³ norm, with a constant depending only on the given coefficients.

noncomputable def NavierStokesR3.PressureFunctionals.pressurePairLinear (i j : Fin 3) (g : ProblemStatement.Space → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : Comparison.ComplexTest →ₗ[ℂ] ℂ

The canonical pressure pairing, as an actual complex-linear map on tests.

Equations

• NavierStokesR3.PressureFunctionals.pressurePairLinear i j g hg = NavierStokesR3.PressureFunctionals.integralPairLinear g (NavierStokesR3.RieszTestOperators.rieszTestLinear i j) ⋯

@[simp]

theorem NavierStokesR3.PressureFunctionals.pressurePairLinear_apply (i j : Fin 3) (g : ProblemStatement.Space → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ψ : Comparison.ComplexTest) : (pressurePairLinear i j g hg) ψ = Comparison.pressurePair i j g ψ

noncomputable def NavierStokesR3.PressureFunctionals.averagedPressureDifference (W0 W1 : ProblemStatement.Space → ℝ) (G : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ) (hW0 : MeasureTheory.MemLp W0 2 MeasureTheory.volume) (hW1 : MeasureTheory.MemLp W1 2 MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.Integrable (G i j) MeasureTheory.volume) (k : Fin 3) : Comparison.ComplexTest →ₗ[ℂ] ℂ

The averaged pressure-gradient difference determined by the stated velocity and quadratic-tensor coefficients.

Equations

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

@[simp]

theorem NavierStokesR3.PressureFunctionals.averagedPressureDifference_apply (W0 W1 : ProblemStatement.Space → ℝ) (G : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ) (hW0 : MeasureTheory.MemLp W0 2 MeasureTheory.volume) (hW1 : MeasureTheory.MemLp W1 2 MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.Integrable (G i j) MeasureTheory.volume) (k : Fin 3) (ψ : Comparison.ComplexTest) : (averagedPressureDifference W0 W1 G hW0 hW1 hG k) ψ = averagedPressureDifferenceValue W0 W1 G k ψ

theorem NavierStokesR3.PressureFunctionals.averagedPressureDifference_bound {W0 W1 : ProblemStatement.Space → ℝ} {G : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ} (hW0 : MeasureTheory.MemLp W0 2 MeasureTheory.volume) (hW1 : MeasureTheory.MemLp W1 2 MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.Integrable (G i j) MeasureTheory.volume) (k : Fin 3) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ψ : Comparison.ComplexTest), ‖(averagedPressureDifference W0 W1 G hW0 hW1 hG k) ψ‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)

The actual complex-linear functional satisfies a uniform H³ estimate.