Real-valued whole-space Lᵖ norms

These lemmas convert extended Lᵖ seminorms to the real-valued norms used by the comparison argument. Bounds that require a finite right-hand norm retain an explicit MemLp hypothesis.

theorem NavierStokesR3.LpNormTools.lpNorm_nonneg {E : Type u_1} [NormedAddCommGroup E] (p : ENNReal) (f : ProblemStatement.Space → E) : 0 ≤ Comparison.comparisonLpNorm p f

theorem NavierStokesR3.LpNormTools.lpNorm_congr_ae {E : Type u_1} [NormedAddCommGroup E] {p : ENNReal} {f g : ProblemStatement.Space → E} (hfg : f =ᵐ[MeasureTheory.volume] g) : Comparison.comparisonLpNorm p f = Comparison.comparisonLpNorm p g

theorem NavierStokesR3.LpNormTools.lpNorm_mono_of_norm_le_ae {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {p : ENNReal} {f : ProblemStatement.Space → E} {g : ProblemStatement.Space → F} (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (hfg : ∀ᵐ (x : ProblemStatement.Space), ‖f x‖ ≤ ‖g x‖) : Comparison.comparisonLpNorm p f ≤ Comparison.comparisonLpNorm p g

theorem NavierStokesR3.LpNormTools.lpNorm_mono_of_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {p : ENNReal} {f : ProblemStatement.Space → E} {g : ProblemStatement.Space → F} (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (hfg : ∀ (x : ProblemStatement.Space), ‖f x‖ ≤ ‖g x‖) : Comparison.comparisonLpNorm p f ≤ Comparison.comparisonLpNorm p g

theorem NavierStokesR3.LpNormTools.lpNorm_add_le {E : Type u_1} [NormedAddCommGroup E] {p : ENNReal} (hp1 : 1 ≤ p) {f g : ProblemStatement.Space → E} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) : (Comparison.comparisonLpNorm p fun (x : ProblemStatement.Space) => f x + g x) ≤ Comparison.comparisonLpNorm p f + Comparison.comparisonLpNorm p g

theorem NavierStokesR3.LpNormTools.lpNorm_const_smul {E : Type u_1} [NormedAddCommGroup E] {𝕜 : Type u_3} [NormedField 𝕜] [NormedSpace 𝕜 E] (p : ENNReal) (c : 𝕜) (f : ProblemStatement.Space → E) : (Comparison.comparisonLpNorm p fun (x : ProblemStatement.Space) => c • f x) = ‖c‖ * Comparison.comparisonLpNorm p f

theorem NavierStokesR3.LpNormTools.lpNorm_one_eq_integral_norm {E : Type u_1} [NormedAddCommGroup E] {f : ProblemStatement.Space → E} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : Comparison.comparisonLpNorm 1 f = ∫ (x : ProblemStatement.Space), ‖f x‖

theorem NavierStokesR3.LpNormTools.lpNorm_two_sq_eq_l2Sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : Comparison.comparisonLpNorm 2 f ^ 2 = Comparison.l2Sq f

theorem NavierStokesR3.LpNormTools.lpNorm_two_eq_sqrt_l2Sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : Comparison.comparisonLpNorm 2 f = √(Comparison.l2Sq f)