Time difference quotients of a strong solution #

For h > 0 put s(x, t) = (x, t + h) and v = (u ∘ s - u) / h, Dv = (Du ∘ s - Du) / h, D²v = (D²u ∘ s - D²u) / h, ∂ₜv = (∂ₜu ∘ s - ∂ₜu) / h, q = (p ∘ s - p) / h, Hᵢⱼ = ((uᵢuⱼ) ∘ s - uᵢuⱼ) / h. On the slab over (t₀, T - h) the difference quotient v has the weak derivatives Dv, D²v, ∂ₜv, all square integrable, is solenoidal, and solves the linear equation ∂ₜv - Δv + div H + ∇q = 0 weakly, with Hᵢⱼ = vᵢ (uⱼ ∘ s) + uᵢ vⱼ. This is the difference-quotient step of the Kiselev–Ladyzhenskaya argument in prop:lps-smoothing; no square integrability of H is used.

source

CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo c d) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => κ • (w₁ z - w₂ z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => κ • (Dw₁ z i - Dw₂ z i)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => κ • (D2w₁ z i j - D2w₂ z i j)) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => κ • (Dtw₁ z - Dtw₂ z)

Space-time weak derivatives are compatible with scaled differences of square integrable fields (prop:lps-smoothing).

source

CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ (T - h)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (1 / h) • (u (z.1, z.2 + h) - u z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => (1 / h) • (Du (z.1, z.2 + h) i - Du z i)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => (1 / h) • (D2u (z.1, z.2 + h) i j - D2u z i j)) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (1 / h) • (Dtu (z.1, z.2 + h) - Dtu z)

The time difference quotient of a strong solution has space-time weak derivatives on the slab over (t₀, T - h), namely the difference quotients of the weak derivatives (prop:lps-smoothing).

source

theorem ESS.LPS.lps_timeDifference_memLp {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {t₀ T h : ℝ} (hh : 0 < h) {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) :

MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (1 / h) • (f (z.1, z.2 + h) - f z)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h))))

The time difference quotient of a square integrable field on the slab over (t₀, T) is square integrable on the slab over (t₀, T - h).

source

φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ (T - h)) → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h)), ∑ i : Fin 3, ((1 / h) • (Dtu (z.1, z.2 + h) - Dtu z)) i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, 1 / h * (u (z.1, z.2 + h) i * u (z.1, z.2 + h) j - u z i * u z j) * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, ((1 / h) • (Du (z.1, z.2 + h) i - Du z i)) j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - 1 / h * (p (z.1, z.2 + h) - p z) * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The time difference quotient of a strong solution solves, on the slab over (t₀, T - h), the linear equation ∂ₜv - Δv + div H + ∇q = 0 in weak form, with the difference quotients H of u ⊗ u and q of the pressure (prop:lps-smoothing).

source

theorem ESS.LPS.lps_timeDifference_div_free {t₀ T h : ℝ} (hh : 0 < h) {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hdiv : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)), ∑ i : Fin 3, Du z i i = 0) :

∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h))), ∑ i : Fin 3, ((1 / h) • (Du (z.1, z.2 + h) i - Du z i)) i = 0

The time difference quotient of a solenoidal field is solenoidal on the slab over (t₀, T - h).

source

theorem ESS.LPS.lps_timeDifference_flux_eq (h : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) :

1 / h * (u (z.1, z.2 + h) i * u (z.1, z.2 + h) j - u z i * u z j) = ((1 / h) • (u (z.1, z.2 + h) - u z)) i * u (z.1, z.2 + h) j + u z i * ((1 / h) • (u (z.1, z.2 + h) - u z)) j

The difference quotient of uᵢuⱼ splits as vᵢ (uⱼ ∘ s) + uᵢ vⱼ with v the difference quotient of u and s the time translation by h.

source

(CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ (T - h)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (1 / h) • (u (z.1, z.2 + h) - u z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => (1 / h) • (Du (z.1, z.2 + h) i - Du z i)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => (1 / h) • (D2u (z.1, z.2 + h) i j - D2u z i j)) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (1 / h) • (Dtu (z.1, z.2 + h) - Dtu z)) ∧ (MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (1 / h) • (u (z.1, z.2 + h) - u z)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h)))) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => (1 / h) • (Du (z.1, z.2 + h) i - Du z i)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h)))) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => (1 / h) • (D2u (z.1, z.2 + h) i j - D2u z i j)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h)))) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (1 / h) • (Dtu (z.1, z.2 + h) - Dtu z)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h)))) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => 1 / h * (p (z.1, z.2 + h) - p z)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h))))) ∧ (∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ (T - h)), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h)), ∑ i : Fin 3, ((1 / h) • (Dtu (z.1, z.2 + h) - Dtu z)) i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, 1 / h * (u (z.1, z.2 + h) i * u (z.1, z.2 + h) j - u z i * u z j) * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, ((1 / h) • (Du (z.1, z.2 + h) i - Du z i)) j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - 1 / h * (p (z.1, z.2 + h) - p z) * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) ∧ (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h))), ∑ i : Fin 3, ((1 / h) • (Du (z.1, z.2 + h) i - Du z i)) i = 0) ∧ ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3), 1 / h * (u (z.1, z.2 + h) i * u (z.1, z.2 + h) j - u z i * u z j) = ((1 / h) • (u (z.1, z.2 + h) - u z)) i * u (z.1, z.2 + h) j + u z i * ((1 / h) • (u (z.1, z.2 + h) - u z)) j

Time difference quotients of a strong solution (prop:lps-smoothing). Let h > 0, s(x, t) = (x, t + h), v = (u ∘ s - u) / h and likewise Dv, D²v, ∂ₜv, q for Du, D²u, ∂ₜu, p, and Hᵢⱼ = ((uᵢuⱼ) ∘ s - uᵢuⱼ) / h. Given the weak derivatives, square integrability, the weak equation with the time derivative and solenoidality of u on the slab over (t₀, T), on the slab over (t₀, T - h): (a) v has the weak derivatives Dv, D²v, ∂ₜv; (b) v, Dv, D²v, ∂ₜv, q are square integrable; (c) ∂ₜv - Δv + div H + ∇q = 0 weakly; (d) v is solenoidal; (e) Hᵢⱼ = vᵢ (uⱼ ∘ s) + uᵢ vⱼ.

Documentation

LeanPool.EscauriazaSereginSverak.LPS.SmoothingShift

Time difference quotients of a strong solution #