All-time spatial slices of the local strong limit #
The regularized H¹ traces and weak slice convergence provide spatial H¹ representatives for the limit at each positive time.
theorem
ESS.LPS.lps_eLpNorm_vec3_le_sum_coordinates
{f : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
MeasureTheory.eLpNorm f 2 MeasureTheory.volume ≤ ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f x i) 2 MeasureTheory.volume
The L² norm of a vector-valued function is at most the sum of the L² norms of its
coordinates.
theorem
ESS.LPS.lps_eLpNorm_matrix_le_sum_coordinates
{f : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
MeasureTheory.eLpNorm f 2 MeasureTheory.volume ≤ ∑ i : Fin 3,
∑ j : Fin 3, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f x i j) 2 MeasureTheory.volume
The L² norm of a matrix-valued function is at most the sum of the L² norms of its
coordinates.
@[instance_reducible]
The product topology on ParabolicPoint for space-time slice differentiability.
Instances For
@[instance_reducible]
The product normed additive group structure used in the slice regularity arguments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
The product real normed-space structure used in the slice regularity arguments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ESS.LPS.lps_regR12_slice_memLp_bounds
(ρ : CKN.Leray.RegMollifierProfile)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hb : CKN.IsInJ b)
(T M : ℝ)
(hT : 0 ≤ T)
(hM : 0 ≤ M)
(hUniformBounds :
∀ (ε : ℝ) (hε : 0 < ε),
have U := CKN.Leray.regR12Velocity ρ ε hε b hb;
have D := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => U y i) j z;
have D2 := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) =>
CKN.spatialPartial
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => U x i) j y)
k z;
(∀ t ∈ Set.Icc 0 T,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t)) ^ 2 + CKN.spatialGradientSq U D (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2 z i j) ^ 2 ≤ M)
(ε : ℝ)
(hε : 0 < ε)
(t : ℝ)
(ht : t ∈ Set.Icc 0 T)
:
MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε b hb (x, t)) 2
MeasureTheory.volume ∧ MeasureTheory.MemLp
(fun (x : CKN.Foundation.Parabolic.Vec3) (i j : Fin 3) =>
CKN.spatialPartial
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε b hb y i) j (x, t))
2 MeasureTheory.volume ∧ (∀ (i : Fin 3),
∃ (hi :
MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε b hb (x, t) i)
2 MeasureTheory.volume),
‖MeasureTheory.MemLp.toLp
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε b hb (x, t) i) hi‖ ≤ √M) ∧ ∀ (i j : Fin 3),
∃ (hij :
MeasureTheory.MemLp
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.spatialPartial
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε b hb y i) j
(x, t))
2 MeasureTheory.volume),
‖MeasureTheory.MemLp.toLp
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.spatialPartial
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε b hb y i) j
(x, t))
hij‖ ≤ √M
theorem
ESS.LPS.lps_strong_limit_all_time_h1_slices
(ρ : CKN.Leray.RegMollifierProfile)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(hb :
(∀ (i : Fin 3),
∃ (h : CKN.H1Function Set.univ),
(h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) ∧ CKN.IsInJ b)
(T M : ℝ)
(hT : 0 < T)
(hM : 0 ≤ M)
(hUniformBounds :
∀ (ε : ℝ) (hε : 0 < ε),
have Uε := CKN.Leray.regR12Velocity ρ ε hε b ⋯;
have Dε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Uε y i) j z;
have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) =>
CKN.spatialPartial
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => Uε x i) j y)
k z;
(∀ t ∈ Set.Icc 0 T,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (Uε (x, t)) ^ 2 + CKN.spatialGradientSq Uε Dε (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2ε z i j) ^ 2 ≤ M)
(σ : ℕ → ℕ)
(hσ : StrictMono σ)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hweakSlice :
∀ (t : ℝ),
0 < t →
∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
MeasureTheory.MemLp w 2 MeasureTheory.volume →
Filter.Tendsto
(fun (n : ℕ) =>
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.Leray.regR12Uε ρ b ⋯ (1 / (↑(σ n) + 1)) (x, t) i * w x i)
Filter.atTop (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i)))
(hrep :
∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ),
0 < z.2 →
u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) = CKN.Leray.compactnessMollifiedLimit
(fun (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
CKN.Leray.regR12Uε ρ b ⋯ (1 / (↑(σ n) + 1)) (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
σ z)
:
∃ (Dslice : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3),
∀ t ∈ Set.Ioc 0 T,
IsLpsGoodTime u Dslice t ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ≤ 9 * ENNReal.ofReal √M ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => Dslice (x, t)) 2 MeasureTheory.volume ≤ 9 * ENNReal.ofReal √M
Uniform regularized H¹ bounds pass to every positive-time slice of the
selected Leray limit. The slices belong to H¹ ∩ J, and the same bounds give
the finite-slab L² control used for the velocity tensor.
theorem
ESS.LPS.lps_strong_limit_h1_slices_closed
{b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hb :
(∀ (i : Fin 3),
∃ (h : CKN.H1Function Set.univ),
(h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) ∧ CKN.IsInJ b)
{T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(htrace : ∀ (x : CKN.Foundation.Parabolic.Vec3), u (x, 0) = b x)
(B : ENNReal)
(Dpositive : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(hpositive :
∀ t ∈ Set.Ioc 0 T,
IsLpsGoodTime u Dpositive t ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ≤ B ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => Dpositive (x, t)) 2 MeasureTheory.volume ≤ B)
:
∃ (Dslice : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3),
(∀ t ∈ Set.Icc 0 T, IsLpsGoodTime u Dslice t) ∧ ∀ t ∈ Set.Ioc 0 T,
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ≤ B ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => Dslice (x, t)) 2 MeasureTheory.volume ≤ B
The initial trace and the datum's H¹ ∩ J representative fill in the
zero-time slice, while the positive-time extraction includes the final time.
This gives selected H¹ ∩ J representatives on the whole closed interval.