The scalar R³ H² estimate used for harmonic interior control.

theorem EulerMeanHarmonic.partialDerivative_twice (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative f i) i x = (iteratedFDeriv ℝ 2 f x) fun (x : Fin 2) => EuclideanSpace.single i 1

theorem EulerMeanHarmonic.complex_eLpNorm_toReal (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : (MeasureTheory.eLpNorm (fun (x : EulerSmoothLimit.Space) => ↑(f x)) 2 MeasureTheory.volume).toReal = MeasureTheory.lpNorm f 2 MeasureTheory.volume

theorem EulerMeanHarmonic.scalar_pointwise_le_H2 (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) (x : EulerSmoothLimit.Space) : |f x| ≤ EulerSobolev.embeddingConstant 3 2 scalar_pointwise_le_H2._proof_1 * (MeasureTheory.lpNorm f 2 MeasureTheory.volume + (2 * Real.pi) ^ (-2) * ∑ i : Fin 3, MeasureTheory.lpNorm (EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative f i) i) 2 MeasureTheory.volume)

This is the existing Fourier Sobolev estimate applied to the actual scalar function and its actual twofold coordinate derivatives, with no embedding estimate supplied as a hypothesis.

theorem EulerMeanHarmonic.lpNorm_sq_eq_integral_norm_sq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2 = ∫ (x : EulerSmoothLimit.Space), ‖f x‖ ^ 2

theorem EulerMeanHarmonic.lpNorm_sq_eq_integral_sq (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2 = ∫ (x : EulerSmoothLimit.Space), f x ^ 2