Harmonic functionals bounded in an inhomogeneous Fourier Sobolev norm

A complex-linear Schwartz functional bounded by the Fourier H³ norm is represented in polynomially weighted L². If it annihilates Laplacians, its representing function vanishes away from the origin. Since volume has no atom at the origin, the whole functional vanishes.

Weak uniqueness for the weighted Fourier representation

Compact smooth functions are Schwartz functions, so a locally integrable function annihilating every Schwartz test vanishes almost everywhere. Applied to the weighted conjugate of an L² function, this removes the Fourier Laplacian multiplier away from its single zero at the origin.

theorem NavierStokesR3.WeakFourierUniqueness.ae_eq_zero_of_integral_real_test_mul_eq_zero (h : ProblemStatement.Space → ℂ) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) (hzero : ∀ (g : ProblemStatement.Space → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → ∫ (x : ProblemStatement.Space), ↑(g x) * h x = 0) : h =ᵐ[MeasureTheory.volume] 0

The real-test fundamental lemma, with multiplication written in ℂ.

theorem NavierStokesR3.WeakFourierUniqueness.ae_eq_zero_of_integral_schwartz_test_mul_eq_zero (h : ProblemStatement.Space → ℂ) (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) (hzero : ∀ (ψ : Comparison.ComplexTest), ∫ (x : ProblemStatement.Space), h x * ψ x = 0) : h =ᵐ[MeasureTheory.volume] 0

A locally integrable function is determined by its Schwartz pairings.

theorem NavierStokesR3.WeakFourierUniqueness.locallyIntegrable_weighted_star (q : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.LocallyIntegrable (fun (ξ : ProblemStatement.Space) => star (↑↑q ξ) * ↑((1 + ‖ξ‖ ^ 2) ^ 2) * ↑(‖ξ‖ ^ 2)) MeasureTheory.volume

Polynomial weights preserve the local integrability of an L² function.

theorem NavierStokesR3.WeakFourierUniqueness.eq_zero_of_integral_weight_normSq_test_eq_zero (q : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hq : ∀ (ψ : Comparison.ComplexTest), ∫ (ξ : ProblemStatement.Space), star (↑↑q ξ) * ↑((1 + ‖ξ‖ ^ 2) ^ 2) * ↑(‖ξ‖ ^ 2) * ψ ξ = 0) : q = 0

If the weighted Fourier Laplacian pairings of an L² function vanish, the function is zero in L². No regularity beyond membership in L² is used.

Hilbert-space representation of a functional bounded through an embedding

A linear functional on a complex vector space that is bounded in the norm of an injective linear map into a Hilbert space is represented by an inner product in that Hilbert space. No topology on the source vector space is needed.

theorem NavierStokesR3.HilbertFunctionalExtension.exists_inner_representation {E : Type u} [AddCommGroup E] [Module ℂ E] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (B : E →ₗ[ℂ] H) (hB : Function.Injective ⇑B) (F : E →ₗ[ℂ] ℂ) {C : ℝ} (hbound : ∀ (x : E), ‖F x‖ ≤ C * ‖B x‖) : ∃ (q : H), ∀ (x : E), F x = inner ℂ q (B x)

Transfer a functional to the range of an injective linear map, extend it by Hahn–Banach, and represent the extension by the Hilbert-space inner product.

@[reducible, inline]

noncomputable abbrev NavierStokesR3.HarmonicTestFunctionals.FrequencyL2 : AddSubgroup (ProblemStatement.Space →ₘ[MeasureTheory.volume] ℂ)

Frequency L²: an abbreviation for Lp ℂ 2 (volume : Measure Space).

Equations

• NavierStokesR3.HarmonicTestFunctionals.FrequencyL2 = MeasureTheory.Lp ℂ 2 MeasureTheory.volume

theorem NavierStokesR3.HarmonicTestFunctionals.exists_inner_representation_of_fourierHNormSq_bound (F : Comparison.ComplexTest →ₗ[ℂ] ℂ) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (ψ : Comparison.ComplexTest), ‖F ψ‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)) : ∃ (q : ↥FrequencyL2), ∀ (ψ : Comparison.ComplexTest), F ψ = inner ℂ q (FourierSobolevWeights.B ψ)

The H³ bound supplies a Hilbert-space representative after a polynomial Fourier embedding. No Fourier transform of arbitrary L² functions is needed.

theorem NavierStokesR3.HarmonicTestFunctionals.continuous_of_fourierHNormSq_bound (F : Comparison.ComplexTest →ₗ[ℂ] ℂ) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (ψ : Comparison.ComplexTest), ‖F ψ‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)) : Continuous ⇑F

In particular, a functional with the stated Fourier bound is continuous for the Schwartz topology.

theorem NavierStokesR3.HarmonicTestFunctionals.representative_eq_zero_of_harmonic (q : ↥FrequencyL2) (hq : ∀ (ψ : Comparison.ComplexTest), inner ℂ q (FourierSobolevWeights.B (laplacianCLM ψ)) = 0) : q = 0

A weighted L² representative that annihilates ordinary Laplacians is zero.

theorem NavierStokesR3.HarmonicTestFunctionals.eq_zero_of_harmonic (F : Comparison.ComplexTest →ₗ[ℂ] ℂ) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (ψ : Comparison.ComplexTest), ‖F ψ‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)) (hharmonic : ∀ (ψ : Comparison.ComplexTest), F (laplacianCLM ψ) = 0) : F = 0

A harmonic Schwartz functional bounded in Fourier H⁻³ vanishes.

theorem NavierStokesR3.HarmonicTestFunctionals.eq_zero_of_compact_harmonic (F : Comparison.ComplexTest →ₗ[ℂ] ℂ) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (ψ : Comparison.ComplexTest), ‖F ψ‖ ≤ C * √(Comparison.fourierHNormSq 3 ψ)) (hharmonic : ∀ (ψ : Comparison.ComplexTest), HasCompactSupport ⇑ψ → F (laplacianCLM ψ) = 0) : F = 0

The pressure-recovery form: harmonicity need only be known against compactly supported tests. The Fourier bound supplies the continuity needed to pass to all Schwartz tests. No pressure pairing outside compact support is assumed.

theorem NavierStokesR3.TemporalTestUniqueness.eq_zero_on_open_of_tests {U : Set ℝ} (hU : IsOpen U) {f : ℝ → ℂ} (hf : ContinuousOn f U) (htest : ∀ (a : ℝ → ℝ), ContDiff ℝ (↑⊤) a → HasCompactSupport a → tsupport a ⊆ U → ∫ (t : ℝ), a t • f t = 0) (t : ℝ) : t ∈ U → f t = 0

Continuity turns the distributional fundamental lemma into equality at every time of the open interval. The tests are real, and values may be complex.