Rellich Balls Core

Supporting estimates for the Navier–Stokes development.

theorem CKN.Foundation.memLp_two_cutoff_vec3_global {K : Set Parabolic.Vec3} (hK : MeasurableSet K) (f : Parabolic.Vec3 → Parabolic.L2Vec3) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict K)) (χ : Parabolic.Vec3 → ℝ) (hχ : Measurable χ) (hχsupport : tsupport χ ⊆ K) (hχbound : ∀ (x : Parabolic.Vec3), |χ x| ≤ 1) : MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => χ x • f x) 2 MeasureTheory.volume

A bounded smooth cutoff turns a local vector-valued L² field into a global L² field when its support lies in the local region.

theorem CKN.Foundation.eLpNorm_two_cutoff_vec3_global_le {K : Set Parabolic.Vec3} (hK : MeasurableSet K) (f : Parabolic.Vec3 → Parabolic.L2Vec3) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict K)) (χ : Parabolic.Vec3 → ℝ) (hχ : Measurable χ) (hχsupport : tsupport χ ⊆ K) (hχbound : ∀ (x : Parabolic.Vec3), |χ x| ≤ 1) : MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => χ x • f x) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict K)

The global L² norm after a cutoff bounded by one does not exceed the local L² norm of the original field.

theorem CKN.Foundation.norm_toLp_two_cutoff_vec3_le {K : Set Parabolic.Vec3} (hK : MeasurableSet K) (f : Parabolic.Vec3 → Parabolic.L2Vec3) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict K)) (χ : Parabolic.Vec3 → ℝ) (hχ : Measurable χ) (hχsupport : tsupport χ ⊆ K) (hχbound : ∀ (x : Parabolic.Vec3), |χ x| ≤ 1) (M : ENNReal) (hM : M < ⊤) (henergy : ∫⁻ (x : Parabolic.Vec3) in K, ‖f x‖ₑ ^ 2 ≤ M) : ‖MeasureTheory.MemLp.toLp (fun (x : Parabolic.Vec3) => χ x • f x) ⋯‖ ≤ (M ^ (1 / 2)).toReal

A local squared-integral bound controls the Hilbert norm of a bounded cutoff of the field.

theorem CKN.Foundation.eLpNorm_two_sub_average_le_of_h1_on_euclidean_ball (x₀ : Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (u : H1Function (euclideanBall x₀ r)) : MeasureTheory.eLpNorm (fun (x : Vec 3) => u.toFun x - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ r)) u.toFun) 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm u.grad 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) * MeasureTheory.volume (euclideanBall x₀ r) ^ (1 / 3)

The weak-gradient ball Poincaré estimate in L⁶ implies the corresponding L² estimate, with the finite-measure factor made explicit. This is the small-ball estimate used in the spatial compactness argument for lem:compactness.

theorem CKN.Foundation.memLp_two_vec3_of_lintegral_sq_lt_top {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → Parabolic.Vec3) (hf : Measurable f) (hfinite : ∫⁻ (x : α), ENNReal.ofReal (Parabolic.vec3EuclideanNorm (f x)) ^ 2 ∂μ < ⊤) : MeasureTheory.MemLp (fun (x : α) => WithLp.toLp 2 (f x)) 2 μ

A finite squared vec3EuclideanNorm integral gives local L² membership in the CKN vector-valued function space.

theorem CKN.Foundation.memLp_two_real_of_lintegral_sq_lt_top {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → ℝ) (hf : Measurable f) (hfinite : ∫⁻ (x : α), ENNReal.ofReal |f x| ^ 2 ∂μ < ⊤) : MeasureTheory.MemLp f 2 μ

A finite squared integral of a measurable real function gives L² membership.

theorem CKN.Foundation.memLp_two_vec3_raw_of_lintegral_sq_lt_top {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → Parabolic.Vec3) (hf : Measurable f) (hfinite : ∫⁻ (x : α), ENNReal.ofReal (Parabolic.vec3EuclideanNorm (f x)) ^ 2 ∂μ < ⊤) : MeasureTheory.MemLp f 2 μ

The same squared-norm bound gives L² membership for Vec3 with its native CKN function-space carrier.

theorem CKN.Foundation.ae_memLp_two_vec3_slice_of_lintegral_sq_lt_top {K : Set Parabolic.Vec3} {J : Set ℝ} (f : Parabolic.ParabolicPoint → Parabolic.Vec3) (hf : Measurable f) (hfinite : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in K, ENNReal.ofReal (Parabolic.vec3EuclideanNorm (f (x, t))) ^ 2 < ⊤) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => WithLp.toLp 2 (f (x, t))) 2 (MeasureTheory.volume.restrict K)

A finite local space-time squared norm gives L² membership of almost every spatial slice.

theorem CKN.Foundation.ae_memLp_two_vec3_raw_slice_of_lintegral_sq_lt_top {K : Set Parabolic.Vec3} {J : Set ℝ} (f : Parabolic.ParabolicPoint → Parabolic.Vec3) (hf : Measurable f) (hfinite : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in K, ENNReal.ofReal (Parabolic.vec3EuclideanNorm (f (x, t))) ^ 2 < ⊤) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => f (x, t)) 2 (MeasureTheory.volume.restrict K)

Finite local space-time squared norm gives native vector-valued L² membership of almost every spatial slice.

theorem CKN.Foundation.memLp_two_spatial_gradient_of_finite_energy {K : Set Parabolic.Vec3} (u : Parabolic.ParabolicPoint → Parabolic.Vec3) (Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3) (t : ℝ) (hDu : Measurable Du) (henergy : ∫⁻ (x : Parabolic.Vec3) in K, ENNReal.ofReal (spatialGradientSq u Du (x, t)) < ⊤) : MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => Du (x, t)) 2 (MeasureTheory.volume.restrict K)

Finite spatial gradient energy gives L² membership of the matrix field on that spatial region.

theorem CKN.Foundation.ae_memLp_two_spatial_gradient_slice_of_lintegral_lt_top {K : Set Parabolic.Vec3} {J : Set ℝ} (u : Parabolic.ParabolicPoint → Parabolic.Vec3) (Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3) (hDu : Measurable Du) (hfinite : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in K, ENNReal.ofReal (spatialGradientSq u Du (x, t)) < ⊤) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => Du (x, t)) 2 (MeasureTheory.volume.restrict K)

Finite local space-time gradient energy gives L² membership of almost every spatial gradient slice.

theorem CKN.Foundation.exists_h1_component_on_euclidean_ball_of_slice_data {U : Set Parabolic.Vec3} {x₀ : Parabolic.Vec3} {r : ℝ} (u : Parabolic.Vec3 → Parabolic.Vec3) (Du : Parabolic.Vec3 → Fin 3 → Parabolic.Vec3) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict U)) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u x i) fun (x : Vec 3) => Du x i) (hball : euclideanBall x₀ r ⊆ U) (i : Fin 3) : ∃ (v : H1Function (euclideanBall x₀ r)), (v.toFun = fun (x : Parabolic.Vec3) => u x i) ∧ v.grad = fun (x : Parabolic.Vec3) => Du x i

Slice bounds and the weak-gradient identity restrict a vector field to a scalar H¹ function on each Euclidean ball. The matrix convention is Du x i j = ∂ⱼ uᵢ.

theorem CKN.Foundation.eLpNorm_two_component_sub_average_le_of_slice_data {U : Set Parabolic.Vec3} {x₀ : Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (u : Parabolic.Vec3 → Parabolic.Vec3) (Du : Parabolic.Vec3 → Fin 3 → Parabolic.Vec3) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict U)) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u x i) fun (x : Vec 3) => Du x i) (hball : euclideanBall x₀ r ⊆ U) (i : Fin 3) : MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => u x i - ⨍ (y : Vec 3) in euclideanBall x₀ r, u y i) 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => Du x i) 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) * MeasureTheory.volume (euclideanBall x₀ r) ^ (1 / 3)

The field-level slice bounds and weak-gradient identities imply the scalar ball-average error estimate on every component. This is the estimate later integrated in time in the local compactness argument.

theorem CKN.Foundation.lintegral_sq_le_of_eLpNorm_two_le {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [ContinuousENorm E] [NormedAddCommGroup F] [ContinuousENorm F] {μ : MeasureTheory.Measure α} {f : α → E} {g : α → F} {C : ENNReal} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hfg : MeasureTheory.eLpNorm f 2 μ ≤ C * MeasureTheory.eLpNorm g 2 μ) : ∫⁻ (x : α), ‖f x‖ₑ ^ 2 ∂μ ≤ C ^ 2 * ∫⁻ (x : α), ‖g x‖ₑ ^ 2 ∂μ

An L² seminorm estimate for scalar functions gives the corresponding inequality between their squared-integral densities.

theorem CKN.Foundation.measurable_average_scalar_slice {B : Set Parabolic.Vec3} (f : Parabolic.ParabolicPoint → ℝ) (hf : Measurable f) : Measurable fun (t : ℝ) => ⨍ (x : Parabolic.Vec3) in B, f (x, t)

Scalar ball averages of a jointly measurable field are measurable in time.

theorem CKN.Foundation.lintegral_prod_sq_le_of_ae_eLpNorm_two_le {K : Set Parabolic.Vec3} {J : Set ℝ} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [ContinuousENorm E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [NormedAddCommGroup F] [ContinuousENorm F] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] {f : Parabolic.ParabolicPoint → E} {g : Parabolic.ParabolicPoint → F} {C : ENNReal} (hf : Measurable f) (hg : Measurable g) (hle : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => f (x, t)) 2 (MeasureTheory.volume.restrict K) ≤ C * MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => g (x, t)) 2 (MeasureTheory.volume.restrict K)) : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in K, ‖f (x, t)‖ₑ ^ 2 ≤ C ^ 2 * ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in K, ‖g (x, t)‖ₑ ^ 2

Almost-everywhere slice L² estimates integrate to the corresponding space-time squared-integral estimate on a product of measurable regions.

theorem CKN.Foundation.ae_eLpNorm_two_component_sub_average_le_of_field_energy {U : Set Parabolic.Vec3} {J : Set ℝ} {x₀ : Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (u : Parabolic.ParabolicPoint → Parabolic.Vec3) (Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3) (huMeas : Measurable u) (hDuMeas : Measurable Du) (huenergy : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in U, ENNReal.ofReal (Parabolic.vec3EuclideanNorm (u (x, t))) ^ 2 < ⊤) (hweak : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u (x, t) i) fun (x : Vec 3) => Du (x, t) i) (henergy : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in U, ENNReal.ofReal (spatialGradientSq u Du (x, t)) < ⊤) (hball : euclideanBall x₀ r ⊆ U) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => u (x, t) i - ⨍ (y : Vec 3) in euclideanBall x₀ r, u (y, t) i) 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => Du (x, t) i) 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) * MeasureTheory.volume (euclideanBall x₀ r) ^ (1 / 3)

The local slice bound, integrated gradient bound, and almost-everywhere weak-gradient identity give the ball-average error estimate on almost every time slice.

theorem CKN.Foundation.lintegral_component_ball_average_error_le_of_field_energy {U : Set Parabolic.Vec3} {J : Set ℝ} {x₀ : Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (u : Parabolic.ParabolicPoint → Parabolic.Vec3) (Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3) (huMeas : Measurable u) (hDuMeas : Measurable Du) (huenergy : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in U, ENNReal.ofReal (Parabolic.vec3EuclideanNorm (u (x, t))) ^ 2 < ⊤) (hweak : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u (x, t) i) fun (x : Vec 3) => Du (x, t) i) (henergy : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Parabolic.Vec3) in U, ENNReal.ofReal (spatialGradientSq u Du (x, t)) < ⊤) (hball : euclideanBall x₀ r ⊆ U) (i : Fin 3) : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Vec 3) in euclideanBall x₀ r, ENNReal.ofReal |u (x, t) i - ⨍ (y : Vec 3) in euclideanBall x₀ r, u (y, t) i| ^ 2 ≤ (sobolevPoincareL6Constant * MeasureTheory.volume (euclideanBall x₀ r) ^ (1 / 3)) ^ 2 * ∫⁻ (t : ℝ) in J, ∫⁻ (x : Vec 3) in euclideanBall x₀ r, ‖Du (x, t) i‖ₑ ^ 2

The almost-everywhere ball Poincaré estimates integrate to a space-time bound for the error from the measurable time-dependent ball averages.