Scalar test functions and component energies for actual R³ vector fields.

theorem EulerMeanHarmonic.scalar_component_memLp (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : MeasureTheory.MemLp u 2 MeasureTheory.volume) (i : Fin 3) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => (u x).ofLp i) 2 MeasureTheory.volume

theorem EulerMeanHarmonic.laplacian_scalar_smul_vector (φ : EulerSmoothLimit.Space → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (v x : EulerSmoothLimit.Space) : Laplacian.laplacian (fun (y : EulerSmoothLimit.Space) => φ y • v) x = Laplacian.laplacian φ x • v

theorem EulerMeanHarmonic.scalarWeakHarmonicOn_of_vector_tests (U : Set EulerSmoothLimit.Space) (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space), HasCompactSupport φ → ContDiff ℝ (↑⊤) φ → tsupport φ ⊆ U → ∫ (x : EulerSmoothLimit.Space), inner ℝ (u x) (Laplacian.laplacian φ x) = 0) (i : Fin 3) : ScalarWeakHarmonicOn U fun (x : EulerSmoothLimit.Space) => (u x).ofLp i

Testing a vector distribution along each fixed coordinate gives scalar weak harmonicity.

theorem EulerMeanHarmonic.sum_component_energy (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : MeasureTheory.MemLp u 2 MeasureTheory.volume) : ∑ i : Fin 3, MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => (u x).ofLp i) 2 MeasureTheory.volume ^ 2 = MeasureTheory.lpNorm u 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.ae_vector_bound_of_component_bounds (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : MeasureTheory.MemLp u 2 MeasureTheory.volume) (U : Set EulerSmoothLimit.Space) (C : ℝ) (hc : ∀ (i : Fin 3), ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ U → (u x).ofLp i ^ 2 ≤ C * MeasureTheory.lpNorm (fun (y : EulerSmoothLimit.Space) => (u y).ofLp i) 2 MeasureTheory.volume ^ 2) : ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ U → ‖u x‖ ^ 2 ≤ C * MeasureTheory.lpNorm u 2 MeasureTheory.volume ^ 2

Uniform component bounds combine without a dimension-dependent loss in the energy.