Uniform Relative Bound

The coefficient in Young's inequality for the conjugate exponents 2 / (1 + θ) and 2 / (1 - θ).

noncomputable def ESS.lpsPowerYoungCoefficient (θ : ℝ) : ℝ

The coefficient in Young's inequality for the conjugate exponents 2 / (1 + θ) and 2 / (1 - θ).

Equations

• ESS.lpsPowerYoungCoefficient θ = ((2 / (1 + θ) / 2) ^ (1 / (2 / (1 + θ))))⁻¹ ^ (2 / (1 - θ)) / (2 / (1 - θ))

theorem ESS.lps_sq_eLpNorm_le {E : Type} [NormedAddCommGroup E] {w : CKN.Foundation.Parabolic.Vec3 → E} (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (S : CKN.Foundation.Parabolic.Vec3 → ℝ) (hpoint : ∀ (x : CKN.Foundation.Parabolic.Vec3), ‖w x‖ ^ 2 ≤ S x) (hSint : MeasureTheory.Integrable S MeasureTheory.volume) : (MeasureTheory.eLpNorm w 2 MeasureTheory.volume).toReal ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), S x

The squared L² norm of a field is bounded by the integral of any integrable pointwise majorant of its squared norm.

theorem ESS.lps_norm_sq_le_sum_sq (w : CKN.Foundation.Parabolic.Vec3) : ‖w‖ ^ 2 ≤ ∑ i : Fin 3, w i ^ 2

The squared sup norm of a vector is at most the sum of squares of its entries.

theorem ESS.lps_norm_sq_le_sum_sq₂ (Dw : Fin 3 → CKN.Foundation.Parabolic.Vec3) : ‖Dw‖ ^ 2 ≤ ∑ i : Fin 3, ∑ j : Fin 3, Dw i j ^ 2

The squared sup norm of a matrix is at most the sum of squares of its entries.

theorem ESS.lps_triple_pointwise_euclidean (u w : CKN.Foundation.Parabolic.Vec3) (Dw : Fin 3 → CKN.Foundation.Parabolic.Vec3) : |∑ i : Fin 3, u i * ∑ j : Fin 3, w j * Dw i j| ≤ 9 * (CKN.Foundation.Parabolic.vec3EuclideanNorm u * ‖w‖ * ‖Dw‖)

Pointwise bound of the trilinear convection form by the Euclidean norm of the first factor and the sup norms of the others.

theorem ESS.lps_slice_relative_bound_finite_uniform {s : ℝ} (hs : 3 < s) {u w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (huMeas : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (huS : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) (ENNReal.ofReal s) MeasureTheory.volume) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hDw2 : MeasureTheory.MemLp Dw 2 MeasureTheory.volume) (hgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i) : |∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * ∑ j : Fin 3, w x j * Dw x i j| ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Dw x i j ^ 2) + lpsPowerYoungCoefficient (3 / s) * (9 * (6 * CKN.gagliardoNirenbergSobolevConstant.toReal) ^ (3 / s)) ^ (2 * s / (s - 3)) * (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u x)) (ENNReal.ofReal s) MeasureTheory.volume).toReal ^ (2 * s / (s - 3)) * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, w x i ^ 2

Fixed-time relative convection estimate for a finite Serrin exponent. The coefficient is the distinguished field's spatial L^s norm raised to the critical power 2s/(s-3), as in lem:lps-comparison.