Calculus of weak spatial derivatives for the vorticity bootstrap #

Differentiating a weak heat equation, the product rule for square-integrable fields with square-integrable weak derivatives, uniqueness of weak derivatives, almost-everywhere convergent subsequences and Fatou bounds, and the linearity and locality of backward mollification. These are the weak-level steps of the bootstrap of thm:vorticity-regularity.

source

theorem ESS.vorticity_exists_subseq_ae {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Finite ι] {f : ι → ℕ → α → ℝ} {F : ι → α → ℝ} (hf : ∀ (i : ι) (n : ℕ), MeasureTheory.MemLp (f i n) 2 μ) (hF : ∀ (i : ι), MeasureTheory.MemLp (F i) 2 μ) (h : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f i n - F i) 2 μ) Filter.atTop (nhds 0)) :

∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (x : α) ∂μ, ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => f i (φ n) x) Filter.atTop (nhds (F i x))

Finitely many L²-convergent sequences have a common subsequence converging almost everywhere.

source

theorem ESS.vorticity_integral_le_of_ae_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : ℕ → α → ℝ} {G : α → ℝ} (hg0 : ∀ (n : ℕ) (x : α), 0 ≤ g n x) (hgi : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (hGm : MeasureTheory.AEStronglyMeasurable G μ) (hlim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => g n x) Filter.atTop (nhds (G x))) {K : ℝ} (hK : ∀ (n : ℕ), ∫ (x : α), g n x ∂μ ≤ K) :

MeasureTheory.Integrable G μ ∧ ∫ (x : α), G x ∂μ ≤ K

Fatou's lemma for nonnegative integrands converging almost everywhere.

source

∀ᵐ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict W, g₁ y = g₂ y

Weak derivatives of the same function on an open set agree almost everywhere there.

source

theorem ESS.vorticity_memLp_mul_bounded {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [OpensMeasurableSpace α] {g φ : α → ℝ} (hg : MeasureTheory.MemLp g 2 μ) (hφ : Continuous φ) (hφb : ∃ (C : ℝ), ∀ (x : α), ‖φ x‖ ≤ C) :

MeasureTheory.MemLp (fun (x : α) => g x * φ x) 2 μ

The product of a square-integrable function with a bounded continuous function is square integrable.

source

theorem ESS.vorticity_spatialPartial_neg {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) :

CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => -f y) j z = -CKN.spatialPartial f j z

The spatial derivative of a negated smooth function.

source

theorem ESS.vorticity_spatialPartial_heatOperator {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (m : Fin 3) (y : CKN.Foundation.Parabolic.Vec3 × ℝ) :

CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => -CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) m y = -CKN.timePartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial ψ m y) y - ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial ψ m y) j j y

The spatial derivative of the heat operator applied to a smooth test is the heat operator applied to the spatial derivative of the test.

source

theorem ESS.vorticity_integrableOn_mul_smooth {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f W MeasureTheory.volume) (hφ : Continuous φ) (hφc : HasCompactSupport φ) :

MeasureTheory.IntegrableOn (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => f y * φ y) W MeasureTheory.volume

Products of an integrable function with a smooth compactly supported function are integrable.

source

ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, w' y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ j : Fin 3, F' j y * CKN.spatialPartial ψ j y

Differentiating a weak heat equation in a spatial direction: if the solution and the source have weak derivatives in that direction, the derivatives solve the weak heat equation with the differentiated source.

source

theorem ESS.vorticityBackBall_subset_cthickening {K : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {δ ε : ℝ} (hε : 0 < ε) (hεδ : 6 * ε ≤ δ) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ K) :

Metric.closedBall (z - CKN.vorticityBackShift ε) ε ⊆ Metric.cthickening δ K

The backward kernel balls of the points of a compact set lie in any fixed closed thickening once the radius is small.

source

theorem ESS.vorticity_spatialPartial_mul {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) :

CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => f y * g y) j z = CKN.spatialPartial f j z * g z + f z * CKN.spatialPartial g j z

The product rule for a spatial derivative of smooth space-time functions.

source

ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f y * g y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (f' y * g y + f y * g' y) * ψ y

The product rule for weak spatial derivatives of square-integrable functions with square-integrable weak derivatives on a bounded open set.

Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.VorticityWeakCalculus

Calculus of weak spatial derivatives for the vorticity bootstrap #