Weak continuity of the local velocity

The momentum identity gives a weakly continuous representative of the velocity in L^3 through the terminal time, as in lem:weak-cont-L3 of the Escauriaza–Seregin–Šverák manuscript.

theorem instFactLeENNRealOfNat_leanPool : Fact (1 ≤ 2)

theorem instFactNeENNRealOfNatTop_leanPool : Fact (2 ≠ ⊤)

def CKN.weakContL3SpatialBall : Set Foundation.Parabolic.Vec3

The spatial ball on which the momentum identities are tested.

Equations

• CKN.weakContL3SpatialBall = CKN.Foundation.Parabolic.vec3Ball 0 1

def CKN.weakContL3InnerClosedBall : Set Foundation.Parabolic.Vec3

The closed spatial ball of radius 7 / 8 inside the weak-continuity test ball.

Equations

• CKN.weakContL3InnerClosedBall = closure (CKN.Foundation.Parabolic.vec3Ball 0 (7 / 8))

theorem CKN.weakContL3_cutoff_exists : ∃ (χ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ tsupport χ ⊆ weakContL3SpatialBall ∧ (∀ (x : Foundation.Parabolic.Vec3), 0 ≤ χ x ∧ χ x ≤ 1) ∧ ∀ x ∈ Foundation.Parabolic.vec3Ball 0 (3 / 4), χ x = 1

A smooth cutoff equals one on the smaller ball and is supported in the test ball.

theorem CKN.weakContL3_scalarTrace_exists {a b t₀ : ℝ} (hab : a < b) (ht₀ : t₀ ∈ Set.Ioo a b) {f g : ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioo a b) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Ioo a b) MeasureTheory.volume) (hweak : HasWeakDerivOn (Set.Ioo a b) f g) : ∃ (ell : ℝ → ℝ), Continuous ell ∧ ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → f t = ell t

A scalar function with a weakly integrable derivative has a continuous almost-everywhere representative.

theorem CKN.weakContL3_productWeakDeriv {a b : ℝ} (μx : MeasureTheory.Measure Foundation.Parabolic.Vec3) [MeasureTheory.SFinite μx] {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : MeasureTheory.Integrable F (μx.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))) (hG : MeasureTheory.Integrable G (μx.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))) (hweak : ∀ (η : ℝ → ℝ), IsIntervalTest (Set.Ioo a b) η → ∫ (z : Foundation.Parabolic.Vec3 × ℝ), -(F z * deriv η z.2) - G z * η z.2 ∂μx.prod (MeasureTheory.volume.restrict (Set.Ioo a b)) = 0) : MeasureTheory.LocallyIntegrableOn (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), F (x, t) ∂μx) (Set.Ioo a b) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), G (x, t) ∂μx) (Set.Ioo a b) MeasureTheory.volume ∧ HasWeakDerivOn (Set.Ioo a b) (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), F (x, t) ∂μx) fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), G (x, t) ∂μx

The spatially integrated momentum pairing inherits its time weak derivative.

def CKN.weakContL3SmoothTest : Submodule ℝ (Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3)

The space of smooth compactly supported spatial L²-valued tests.

Equations

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

def CKN.weakContL3SmoothLpSet (μ : MeasureTheory.Measure Foundation.Parabolic.Vec3) : Set ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 μ)

The L² classes admitting a smooth, compactly supported representative.

Equations

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

theorem CKN.weakContL3_smoothTest_memLp {μ : MeasureTheory.Measure Foundation.Parabolic.Vec3} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (φ : ↥weakContL3SmoothTest) : MeasureTheory.MemLp (↑φ) 2 μ

Smooth compactly supported spatial tests define elements of spatial L².

theorem CKN.weakContL3_exists_countable_dense_tests (μ : MeasureTheory.Measure Foundation.Parabolic.Vec3) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ∃ (ψ : ℕ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3), (∀ (n : ℕ), HasCompactSupport (ψ n) ∧ ContDiff ℝ (↑⊤) (ψ n)) ∧ ∃ (hψ : ∀ (n : ℕ), MeasureTheory.MemLp (ψ n) 2 μ), DenseRange fun (n : ℕ) => MeasureTheory.MemLp.toLp (ψ n) ⋯

A countable family of smooth compactly supported tests is dense in spatial L².

noncomputable def CKN.weakContL3OfLp : Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.Vec3

Convert the L² normed encoding of Vec3 to its coordinate representation.

Equations

• CKN.weakContL3OfLp = ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ)

noncomputable def CKN.weakContL3VecToLp : Foundation.Parabolic.Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

The canonical continuous linear map from velocity vectors to L² vectors.

Equations

• CKN.weakContL3VecToLp = ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ).symm

noncomputable def CKN.weakContL3CutoffTest (χ : Foundation.Parabolic.Vec3 → ℝ) (φ : ↥weakContL3SmoothTest) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

Multiply a smooth spatial test by the fixed scalar cutoff.

Equations

• CKN.weakContL3CutoffTest χ φ x = χ x • CKN.weakContL3OfLp (↑φ x)

noncomputable def CKN.weakContL3MomentumPairing (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (χ : Foundation.Parabolic.Vec3 → ℝ) (φ : ↥weakContL3SmoothTest) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The spatial velocity pairing used in the momentum identity.

Equations

• CKN.weakContL3MomentumPairing u χ φ z = ∑ i : Fin 3, u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i * CKN.weakContL3CutoffTest χ φ z.1 i

noncomputable def CKN.weakContL3MomentumFlux (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (χ : Foundation.Parabolic.Vec3 → ℝ) (φ : ↥weakContL3SmoothTest) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The spatial momentum flux paired with a compactly supported test.

Equations

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

theorem CKN.weakContL3_momentumTerms_integrable {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {μx : MeasureTheory.Measure Foundation.Parabolic.Vec3} [MeasureTheory.IsFiniteMeasure μx] {μt : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μt] (hU4 : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (Foundation.Parabolic.parabolicHomeomorph.symm z)) 4 (μx.prod μt)) (hDu2 : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => Du (Foundation.Parabolic.parabolicHomeomorph.symm z)) 2 (μx.prod μt)) (hp : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => p (Foundation.Parabolic.parabolicHomeomorph.symm z)) (ENNReal.ofReal (3 / 2)) (μx.prod μt)) {χ : Foundation.Parabolic.Vec3 → ℝ} (hχsmooth : ContDiff ℝ (↑⊤) χ) (hχcompact : HasCompactSupport χ) (φ : ↥weakContL3SmoothTest) : MeasureTheory.Integrable (weakContL3MomentumPairing u χ φ) (μx.prod μt) ∧ MeasureTheory.Integrable (weakContL3MomentumFlux u Du p χ φ) (μx.prod μt)

The velocity pairing and momentum flux are integrable for smooth spatial tests.

theorem CKN.weakContL3_momentum_gives_productWeak {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hS3 : ∀ Φ ∈ spaceTimeTestFunction weakContL3SpatialBall (Set.Ioo (-1) 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet weakContL3SpatialBall (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Φ y i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Φ y i) i z = 0) {χ : Foundation.Parabolic.Vec3 → ℝ} (hχsmooth : ContDiff ℝ (↑⊤) χ) (hχcompact : HasCompactSupport χ) (hχsupport : tsupport χ ⊆ weakContL3SpatialBall) (φ : ↥weakContL3SmoothTest) (η : ℝ → ℝ) : IsIntervalTest (Set.Ioo (-1) 0) η → ∫ (z : Foundation.Parabolic.Vec3 × ℝ), -(weakContL3MomentumPairing u χ φ z * deriv η z.2) - weakContL3MomentumFlux u Du p χ φ z * η z.2 ∂(MeasureTheory.volume.restrict weakContL3SpatialBall).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) = 0

The momentum identity gives a one-dimensional weak derivative for each spatial test.