Boundary terms of the momentum equation

The weak momentum equation tested with a time cutoff picks up a boundary term at the cut; this module identifies it through the slice pairing of the velocity with the test field (lem:lps-continuation).

noncomputable def ESS.lpsEqIntegrand (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The integrand of the weak momentum equation of a strong solution tested with a vector field φ.

Equations

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

theorem ESS.lps_eqIntegrand_cutoff {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {η : ℝ → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hφ : ContDiff ℝ (↑⊤) φ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : lpsEqIntegrand u Du p (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => η y.2 • φ y) z = η z.2 * lpsEqIntegrand u Du p φ z - deriv η z.2 * ∑ i : Fin 3, u z i * φ z i

Multiplying the test field by a smooth function of time adds only the boundary pairing to the equation integrand.

theorem ESS.lps_eqIntegrand_integrable {a b a₀ c : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hp : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a₀ c)) : MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => lpsEqIntegrand u Du p φ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b))) ∧ MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) i * φ q i) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))

The equation integrand of a strong solution tested with a test field is integrable on the slab, and so is the pairing of the velocity with the field.

theorem ESS.lps_equation_cutoff_integral {a b a₀ c : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {S : (CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) → Prop} (hS : ∀ (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (η : ℝ → ℝ), ContDiff ℝ (↑⊤) η → S φ → S fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => η z.2 • φ z) (hEq : ∀ ψ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), S ψ → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), lpsEqIntegrand u Du p ψ z = 0) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a₀ c)) (hSφ : S φ) {η : ℝ → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hmem : (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => η z.2 • φ z) ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)) : ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), η q.2 * lpsEqIntegrand u Du p φ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) - deriv η q.2 * ∑ i : Fin 3, u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) i * φ q i ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)) = 0

The cutoff-tested equation integral, expressed with the boundary pairing.

theorem ESS.lps_slice_limit_right {a b ℓ : ℝ} {f : ℝ → ℝ} (h : Filter.Tendsto f (nhdsWithin b (Set.Icc a b)) (nhds ℓ)) (δ : ℝ) : δ > 0 → ∃ η > 0, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), b - η < t → |f t - ℓ| < δ

A limit along the closed interval gives the almost-everywhere approximate form used by the boundary-term lemmas.

theorem ESS.lps_slice_limit_left {a b ℓ : ℝ} {f : ℝ → ℝ} (h : Filter.Tendsto f (nhdsWithin a (Set.Icc a b)) (nhds ℓ)) (δ : ℝ) : δ > 0 → ∃ η > 0, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), t < a + η → |f t - ℓ| < δ

The left-end version of lps_slice_limit_right.

theorem ESS.lps_equation_boundary_right {a b c ℓ : ℝ} (hab : a < b) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {S : (CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) → Prop} (hS : ∀ (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (η : ℝ → ℝ), ContDiff ℝ (↑⊤) η → S φ → S fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => η z.2 • φ z) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hp : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hEq : ∀ ψ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), S ψ → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), lpsEqIntegrand u Du p ψ z = 0) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c)) (hSφ : S φ) (hG : ∀ δ > 0, ∃ η > 0, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), b - η < t → |(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * φ (x, t) i) - ℓ| < δ) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), lpsEqIntegrand u Du p φ z = -ℓ

Boundary term of the momentum equation at the right end of a slab: if the equation holds for the test fields supported inside the slab, then tested with a field that need not vanish at the end time it equals minus the slice pairing at that time (lem:lps-continuation).

theorem ESS.lps_equation_boundary_left {a b ℓ : ℝ} (hab : a < b) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {S : (CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) → Prop} (hS : ∀ (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (η : ℝ → ℝ), ContDiff ℝ (↑⊤) η → S φ → S fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => η z.2 • φ z) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hp : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hEq : ∀ ψ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), S ψ → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), lpsEqIntegrand u Du p ψ z = 0) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {a₀ : ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a₀ b)) (hSφ : S φ) (hG : ∀ δ > 0, ∃ η > 0, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), t < a + η → |(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * φ (x, t) i) - ℓ| < δ) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), lpsEqIntegrand u Du p φ z = ℓ

Boundary term of the momentum equation at the left end of a slab (lem:lps-continuation).