Related estimates used together by the same construction modules.

Interpolation for the comparison cutoff weights

These estimates interpolate the unweighted L² norm of a vector field with the L⁶ norm after multiplication by the fourth power of a cutoff. They use only measurability and finite endpoint norms. In fact, the interpolation identities only require a nonnegative weight; an upper bound of one is unnecessary.

theorem NavierStokesR3.WeightedInterpolation.eLpNorm_le_rpow_mul {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {f : ProblemStatement.Space → E} {g : ProblemStatement.Space → F} {h : ProblemStatement.Space → G} {p q r : ENNReal} {a b : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hp : 0 < p.toReal) (hq : 0 < q.toReal) (hr : 0 < r.toReal) (ha : 0 < a) (hb : 0 < b) (hra : r.toReal < p.toReal / a) (hab : 1 / r.toReal = 1 / (p.toReal / a) + 1 / (q.toReal / b)) (hh : ∀ᵐ (x : ProblemStatement.Space), ‖h x‖ ≤ ‖f x‖ ^ a * ‖g x‖ ^ b) : MeasureTheory.eLpNorm h r MeasureTheory.volume ≤ MeasureTheory.eLpNorm f p MeasureTheory.volume ^ a * MeasureTheory.eLpNorm g q MeasureTheory.volume ^ b

Hölder interpolation for a function dominated by a product of powers. The arithmetic assumptions are on real exponents, so rational specializations can be discharged by norm_num.

theorem NavierStokesR3.WeightedInterpolation.memLp_and_lpNorm_le_rpow_mul {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {f : ProblemStatement.Space → E} {g : ProblemStatement.Space → F} {h : ProblemStatement.Space → G} {p q r : ENNReal} {a b : ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g q MeasureTheory.volume) (hhm : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) (hp : 0 < p.toReal) (hq : 0 < q.toReal) (hr : 0 < r.toReal) (ha : 0 < a) (hb : 0 < b) (hra : r.toReal < p.toReal / a) (hab : 1 / r.toReal = 1 / (p.toReal / a) + 1 / (q.toReal / b)) (hh : ∀ᵐ (x : ProblemStatement.Space), ‖h x‖ ≤ ‖f x‖ ^ a * ‖g x‖ ^ b) : MeasureTheory.MemLp h r MeasureTheory.volume ∧ Comparison.comparisonLpNorm r h ≤ Comparison.comparisonLpNorm p f ^ a * Comparison.comparisonLpNorm q g ^ b

The preceding estimate also proves membership at the interpolated exponent and permits passage to the real-valued comparison norm.

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

The real-valued seminorm is nonnegative.

theorem NavierStokesR3.WeightedInterpolation.integral_norm_rpow_eq_lpNorm_rpow {E : Type u_1} [NormedAddCommGroup E] {f : ProblemStatement.Space → E} {p : ENNReal} (hp : 0 < p.toReal) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ∫ (x : ProblemStatement.Space), ‖f x‖ ^ p.toReal = Comparison.comparisonLpNorm p f ^ p.toReal

Recover the integral of a norm power from the finite real-valued seminorm.

theorem NavierStokesR3.WeightedInterpolation.pow_four_rpow {x : ℝ} (hx : 0 ≤ x) (k : ℕ) : (x ^ 4) ^ (↑k / 4) = x ^ k

The fourth-power cutoff has exactly the required fractional powers.

theorem NavierStokesR3.WeightedInterpolation.norm_weight_pow_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ} (hφ : 0 ≤ φ) (w : E) (k : ℕ) : ‖φ ^ k • w‖ = ‖w‖ ^ (1 - ↑k / 4) * ‖φ ^ 4 • w‖ ^ (↑k / 4)

Pointwise factorization underlying all three interpolation estimates.

theorem NavierStokesR3.WeightedInterpolation.cutoff_interpolation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → E} {k : ℕ} {r : ENNReal} (hφm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume) (hφ : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hweighted : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) 6 MeasureTheory.volume) (hr : 0 < r.toReal) (ha : 0 < 1 - ↑k / 4) (hb : 0 < ↑k / 4) (hra : r.toReal < 2 / (1 - ↑k / 4)) (hab : 1 / r.toReal = 1 / (2 / (1 - ↑k / 4)) + 1 / (6 / (↑k / 4))) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ k • w x) r MeasureTheory.volume ∧ (Comparison.comparisonLpNorm r fun (x : ProblemStatement.Space) => φ x ^ k • w x) ≤ Comparison.comparisonLpNorm 2 w ^ (1 - ↑k / 4) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ^ (↑k / 4)

A generic cutoff interpolation theorem with explicit exponent arithmetic.

theorem NavierStokesR3.WeightedInterpolation.cutoff_interpolation_twelve_fifths {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → E} (hφm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume) (hφ : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hweighted : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) 6 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x • w x) (12 / 5) MeasureTheory.volume ∧ (Comparison.comparisonLpNorm (12 / 5) fun (x : ProblemStatement.Space) => φ x • w x) ≤ Comparison.comparisonLpNorm 2 w ^ (3 / 4) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ^ (1 / 4)

φ w belongs to L^(12/5) with the exact endpoint interpolation bound.

theorem NavierStokesR3.WeightedInterpolation.cutoff_interpolation_three {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → E} (hφm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume) (hφ : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hweighted : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) 6 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 2 • w x) 3 MeasureTheory.volume ∧ (Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => φ x ^ 2 • w x) ≤ Comparison.comparisonLpNorm 2 w ^ (1 / 2) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ^ (1 / 2)

φ² w belongs to L³ with the exact endpoint interpolation bound.

theorem NavierStokesR3.WeightedInterpolation.cutoff_interpolation_four {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → E} (hφm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume) (hφ : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hweighted : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) 6 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 3 • w x) 4 MeasureTheory.volume ∧ (Comparison.comparisonLpNorm 4 fun (x : ProblemStatement.Space) => φ x ^ 3 • w x) ≤ Comparison.comparisonLpNorm 2 w ^ (1 / 4) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ^ (3 / 4)

φ³ w belongs to L⁴ with the exact endpoint interpolation bound.

theorem NavierStokesR3.WeightedInterpolation.cutoff_transport_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → E} (hφm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume) (hφ : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hweighted : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) 6 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => φ x ^ 6 * ‖w x‖ ^ 3) MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), φ x ^ 6 * ‖w x‖ ^ 3 ≤ Comparison.comparisonLpNorm 2 w ^ (3 / 2) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ^ (3 / 2)

The weighted cubic transport integrand is integrable and controlled by the two endpoint norms.

Transport and pressure with a compact spatial weight

Only the scalar weight has compact support. The velocity, transported field, and pressure may be arbitrary smooth functions on Euclidean three-space.

theorem NavierStokesR3.LocalizedDifferenceEnergy.divergence_weighted {χ : NavierStokes.ProblemStatement.Space → ℝ} {v : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hv : ContDiff ℝ (↑⊤) v) (x : NavierStokes.ProblemStatement.Space) : ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => χ y • v y) x).ofLp i = (fderiv ℝ χ x) (v x) + χ x * ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i v x).ofLp i

The divergence of a scalar-weighted vector field.

theorem NavierStokesR3.LocalizedDifferenceEnergy.integral_weighted_fderiv_apply {χ f : NavierStokes.ProblemStatement.Space → ℝ} {v : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (hcχ : HasCompactSupport χ) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i v x).ofLp i = 0) : ∫ (x : NavierStokes.ProblemStatement.Space), χ x * (fderiv ℝ f x) (v x) = -∫ (x : NavierStokes.ProblemStatement.Space), f x * (fderiv ℝ χ x) (v x)

A compact scalar weight transfers a directional derivative to the weight when the vector field is divergence free.

theorem NavierStokesR3.LocalizedDifferenceEnergy.integral_weighted_transport {χ : NavierStokes.ProblemStatement.Space → ℝ} {w v : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) (hv : ContDiff ℝ (↑⊤) v) (hcχ : HasCompactSupport χ) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i v x).ofLp i = 0) : ∫ (x : NavierStokes.ProblemStatement.Space), χ x * inner ℝ (w x) ((fderiv ℝ w x) (v x)) = -(1 / 2) * ∫ (x : NavierStokes.ProblemStatement.Space), ‖w x‖ ^ 2 * (fderiv ℝ χ x) (v x)

The transport energy becomes a flux through the compact weight. No support or global integrability assumption is imposed on either vector field.

theorem NavierStokesR3.LocalizedDifferenceEnergy.integral_weighted_pressure {χ π : NavierStokes.ProblemStatement.Space → ℝ} {w : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hπ : ContDiff ℝ (↑⊤) π) (hw : ContDiff ℝ (↑⊤) w) (hcχ : HasCompactSupport χ) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i w x).ofLp i = 0) : ∫ (x : NavierStokes.ProblemStatement.Space), χ x * (fderiv ℝ π x) (w x) = -∫ (x : NavierStokes.ProblemStatement.Space), π x * (fderiv ℝ χ x) (w x)

The pressure term becomes a flux through the compact weight. The pressure need not have compact support or satisfy any bound at infinity.

Finite-energy bounds for whole-space comparison

The hypotheses in this module concern only square integrability and measurability. In particular, the comparison field need not have compact support or any globally bounded derivative.

theorem NavierStokesR3.Comparison.squareIntegrableAtTime_iff_memLp {u : ProblemStatement.VelocityField} {t : ℝ} (hu : MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => u (t, x)) MeasureTheory.volume) : ProblemStatement.SquareIntegrableAtTime u t ↔ MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => u (t, x)) 2 MeasureTheory.volume

The explicit square-integrability condition is the usual MemLp condition once measurability of the velocity slice is known.

theorem NavierStokesR3.Comparison.continuous_slice_of_continuousOn {times : Set ℝ} {u : ProblemStatement.VelocityField} (hu : ContinuousOn u (times ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ times) : Continuous fun (x : ProblemStatement.Space) => u (t, x)

Joint continuity on a time slab gives continuity of every spatial slice, including a boundary time.

theorem NavierStokesR3.Comparison.l2Sq_nonneg {E : Type u_1} [NormedAddCommGroup E] (f : ProblemStatement.Space → E) : 0 ≤ l2Sq f

No integrability hypothesis is needed for nonnegativity of the totalized integral defining the squared norm.

theorem NavierStokesR3.Comparison.norm_sub_sq_le_twice {E : Type u_1} [SeminormedAddCommGroup E] (a b : E) : ‖a - b‖ ^ 2 ≤ 2 * (‖a‖ ^ 2 + ‖b‖ ^ 2)

The elementary pointwise estimate used for the difference energy.

theorem NavierStokesR3.Comparison.squareIntegrableAtTime_sub {u v : ProblemStatement.VelocityField} {t : ℝ} (hu_meas : MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => u (t, x)) MeasureTheory.volume) (hv_meas : MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => v (t, x)) MeasureTheory.volume) (hu : ProblemStatement.SquareIntegrableAtTime u t) (hv : ProblemStatement.SquareIntegrableAtTime v t) : ProblemStatement.SquareIntegrableAtTime (fun (z : NavierStokes.ProblemStatement.SpaceTime) => u z - v z) t

A difference of square-integrable slices remains square integrable.

theorem NavierStokesR3.Comparison.l2Sq_sub_le {E : Type u_1} [NormedAddCommGroup E] {f g : ProblemStatement.Space → E} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : (l2Sq fun (x : ProblemStatement.Space) => f x - g x) ≤ 2 * (l2Sq f + l2Sq g)

The squared L² norm of a difference is bounded by the two original energies.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_sub {times : Set ℝ} {u v : ProblemStatement.VelocityField} (hu_meas : ∀ t ∈ times, MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => u (t, x)) MeasureTheory.volume) (hv_meas : ∀ t ∈ times, MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => v (t, x)) MeasureTheory.volume) (hu : ProblemStatement.UniformFiniteEnergy times u) (hv : ProblemStatement.UniformFiniteEnergy times v) : ProblemStatement.UniformFiniteEnergy times fun (z : NavierStokes.ProblemStatement.SpaceTime) => u z - v z

Uniform finite energy is stable under taking the velocity difference.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_sub_of_continuousOn {times : Set ℝ} {u v : ProblemStatement.VelocityField} (hu_cont : ContinuousOn u (times ×ˢ Set.univ)) (hv_cont : ContinuousOn v (times ×ˢ Set.univ)) (hu : ProblemStatement.UniformFiniteEnergy times u) (hv : ProblemStatement.UniformFiniteEnergy times v) : ProblemStatement.UniformFiniteEnergy times fun (z : NavierStokes.ProblemStatement.SpaceTime) => u z - v z

The preceding result applies to fields jointly continuous on the slab.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_l2Sq_bound {times : Set ℝ} {u : ProblemStatement.VelocityField} (hu : ProblemStatement.UniformFiniteEnergy times u) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ times, ProblemStatement.SquareIntegrableAtTime u t ∧ (l2Sq fun (x : ProblemStatement.Space) => u (t, x)) ≤ M

A kinetic-energy bound is also a bound for the squared L² norm.

theorem NavierStokesR3.Comparison.norm_component_mul_le_sq (a : ProblemStatement.Space) (i j : Fin 3) : ‖a.ofLp i * a.ofLp j‖ ≤ ‖a‖ ^ 2

Every component product is dominated by the Euclidean squared norm.

theorem NavierStokesR3.Comparison.tensorDiff_norm_le (u v : ProblemStatement.VelocityField) (t : ℝ) (i j : Fin 3) (x : ProblemStatement.Space) : ‖tensorDiff u v t i j x‖ ≤ ‖u (t, x)‖ ^ 2 + ‖v (t, x)‖ ^ 2

Pointwise domination of the nonlinear tensor by the two energy densities.

theorem NavierStokesR3.Comparison.tensorDiff_aestronglyMeasurable {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => u (t, x)) MeasureTheory.volume) (hv : MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => v (t, x)) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.AEStronglyMeasurable (tensorDiff u v t i j) MeasureTheory.volume

The nonlinear tensor has measurable components whenever both velocities have measurable spatial slices.

theorem NavierStokesR3.Comparison.tensorDiff_integrable {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => u (t, x)) 2 MeasureTheory.volume) (hv : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => v (t, x)) 2 MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.Integrable (tensorDiff u v t i j) MeasureTheory.volume

Every component of the tensor difference lies in L¹.

theorem NavierStokesR3.Comparison.tensorDiff_norm_integral_le {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => u (t, x)) 2 MeasureTheory.volume) (hv : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => v (t, x)) 2 MeasureTheory.volume) (i j : Fin 3) : ∫ (x : ProblemStatement.Space), ‖tensorDiff u v t i j x‖ ≤ (l2Sq fun (x : ProblemStatement.Space) => u (t, x)) + l2Sq fun (x : ProblemStatement.Space) => v (t, x)

Its L¹ norm is bounded using only the two ordinary energies.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_tensorDiff_bound {times : Set ℝ} {u v : ProblemStatement.VelocityField} (hu_meas : ∀ t ∈ times, MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => u (t, x)) MeasureTheory.volume) (hv_meas : ∀ t ∈ times, MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => v (t, x)) MeasureTheory.volume) (hu : ProblemStatement.UniformFiniteEnergy times u) (hv : ProblemStatement.UniformFiniteEnergy times v) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ times, ∀ (i j : Fin 3), MeasureTheory.Integrable (tensorDiff u v t i j) MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖tensorDiff u v t i j x‖ ≤ M

A single L¹ bound works for all times and all tensor components.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_lpNorm_two_bound {times : Set ℝ} {u : ProblemStatement.VelocityField} (hu_meas : ∀ t ∈ times, MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => u (t, x)) MeasureTheory.volume) (hu : ProblemStatement.UniformFiniteEnergy times u) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ times, MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => u (t, x)) 2 MeasureTheory.volume ∧ (comparisonLpNorm 2 fun (x : ProblemStatement.Space) => u (t, x)) ≤ M

The finite energy hypothesis gives a uniform bound for the ordinary L² norm, with membership in L² recorded explicitly.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_tensorDiff_lpNorm_one_bound {times : Set ℝ} {u v : ProblemStatement.VelocityField} (hu_meas : ∀ t ∈ times, MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => u (t, x)) MeasureTheory.volume) (hv_meas : ∀ t ∈ times, MeasureTheory.AEStronglyMeasurable (fun (x : ProblemStatement.Space) => v (t, x)) MeasureTheory.volume) (hu : ProblemStatement.UniformFiniteEnergy times u) (hv : ProblemStatement.UniformFiniteEnergy times v) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ times, ∀ (i j : Fin 3), MeasureTheory.Integrable (tensorDiff u v t i j) MeasureTheory.volume ∧ comparisonLpNorm 1 (tensorDiff u v t i j) ≤ M

The uniform tensor estimate in the common comparisonLpNorm notation.