Spatial Sobolev slices for time regularity

The weak spatial derivative and slice-disintegration lemmas used by the all-order time-regularity argument.

@[instance_reducible]

def ESS.LPS.smoothingTimeRegularitySpatialPointNormedAddCommGroup : NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

The product norm on space-time points used for spatial Sobolev slices.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def ESS.LPS.smoothingTimeRegularitySpatialPointNormedSpace : NormedSpace ℝ CKN.Foundation.Parabolic.ParabolicPoint

The real product normed-space structure used for spatial Sobolev slices.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.LPS.lps_velocityTensor_component_hasWeakGradientOn (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (D : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (hD : ∀ (i : Fin 3), CKN.IsSobolevFamilyOn 1 Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (D i)) {L : ℝ} (hbound : ∀ (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3), |u x i| ≤ L) (i j : Fin 3) : (CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u x i * u x j) fun (x : CKN.Vec 3) (k : Fin 3) => D i [k] x * u x j + u x i * D j [k] x) ∧ ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => D i [k] x * u x j + u x i * D j [k] x) 2 MeasureTheory.volume

A bounded H¹ velocity slice has an L² weak gradient for each component of its tensor product (eq:lps-Hm-energy).

theorem ESS.LPS.lps_velocityTensor_divergence_memLp (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (D : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (hD : ∀ (i : Fin 3), CKN.IsSobolevFamilyOn 1 Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (D i)) {L : ℝ} (hbound : ∀ (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3), |u x i| ≤ L) (i : Fin 3) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, (D i [j] x * u x j + u x i * D j [j] x)) 2 MeasureTheory.volume

The divergence of the velocity tensor is spatially L² for a bounded H¹ slice (prop:lps-smoothing).

theorem ESS.LPS.lps_spatialLaplacian_memLp {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hD : CKN.IsSobolevFamilyOn 2 Set.univ f D) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, D [j, j] x) 2 MeasureTheory.volume

The spatial Laplacian of an H² slice belongs to spatial L² (prop:lps-smoothing).

theorem ESS.LPS.lps_sobolevFamily_slice_memLp_ae {m : ℕ} {I : Set ℝ} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hD : CKN.IsL2SobolevFamilyOn m Set.univ I f D) (α : List (Fin 3)) (hα : α.length ≤ m) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => D α (x, t)) 2 MeasureTheory.volume

Every ordered derivative in a space-time L²(I; H^m) family has an spatial L² representative on almost every time slice.

theorem ESS.LPS.lps_sobolevFamily_allSlices_memLp_ae {m : ℕ} {I : Set ℝ} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hD : CKN.IsL2SobolevFamilyOn m Set.univ I f D) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => D α (x, t)) 2 MeasureTheory.volume

The slice representatives supplied by an L²(I; H^m) family are simultaneously square-integrable for all ordered words through order m.

theorem ESS.LPS.lps_sobolevFamily_slice_weak_partial_ae {a b : ℝ} {m : ℕ} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hD : CKN.IsL2SobolevFamilyOn m Set.univ (Set.Ioo a b) f D) (α : List (Fin 3)) (j : Fin 3) (hα : α.length < m) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), CKN.HasWeakPartialDerivOn Set.univ j (fun (x : CKN.Vec 3) => D α (x, t)) fun (x : CKN.Vec 3) => D (α ++ [j]) (x, t)

A space-time weak spatial derivative in an L²(I; H^m) family is a weak derivative on almost every spatial slice.

theorem ESS.LPS.lps_sobolevFamily_spatialSlices_ae {a b : ℝ} {m : ℕ} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hD : CKN.IsL2SobolevFamilyOn m Set.univ (Set.Ioo a b) f D) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), CKN.IsSobolevFamilyOn m Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) fun (α : List (Fin 3)) (x : CKN.Foundation.Parabolic.Vec3) => D α (x, t)

An L²(I; H^m) space-time family restricts to a spatial Sobolev family on almost every time slice.

theorem ESS.LPS.lps_sobolevProvider_spatialSlices {t₀ t₁ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hspatial : ∀ (m : ℕ) (δ : ℝ), 0 < δ → δ < t₁ - t₀ → ∃ (D : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (B : ℝ), 0 ≤ B ∧ (∀ (i : Fin 3), CKN.IsL2SobolevFamilyOn m Set.univ (Set.Ioo (t₀ + δ) t₁) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) (D i)) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) t₁), ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords m, ∫ (x : CKN.Foundation.Parabolic.Vec3), D i α (x, t) ^ 2 ≤ B) (m : ℕ) (δ : ℝ) (hδ : 0 < δ) (hδT : δ < t₁ - t₀) : ∃ (D : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (B : ℝ), 0 ≤ B ∧ (∀ (i : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) t₁), CKN.IsSobolevFamilyOn m Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) fun (α : List (Fin 3)) (x : CKN.Foundation.Parabolic.Vec3) => D i α (x, t)) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) t₁), ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords m, ∫ (x : CKN.Foundation.Parabolic.Vec3), D i α (x, t) ^ 2 ≤ B

The agreed all-order spatial provider yields slice Sobolev families with the same uniform energy bound on every positive-time slab.

theorem ESS.LPS.realLerayProjectionCLM_contDiff_comp {n : ℕ∞} {I : Set ℝ} {f : ℝ → ↥CKN.Leray.RealVectorL2} (hf : ContDiffOn ℝ (↑n) f I) : ContDiffOn ℝ (↑n) (fun (t : ℝ) => realLerayProjectionCLM (f t)) I

A continuously differentiable spatial L² curve remains continuously differentiable after Leray projection (prop:lps-smoothing).

theorem ESS.LPS.realLerayProjectionCLM_hasDerivAt {f f' : ℝ → ↥CKN.Leray.RealVectorL2} {t : ℝ} (hf : HasDerivAt f (f' t) t) : HasDerivAt (fun (s : ℝ) => realLerayProjectionCLM (f s)) (realLerayProjectionCLM (f' t)) t

Pointwise differentiation commutes with the spatial Leray projection on a spatial L² curve (prop:lps-smoothing).