Gluing weak derivative identities

A weak derivative identity which holds for test functions supported in a neighbourhood of every point of an open set holds for every test function supported in the set: a smooth partition of unity subordinate to the neighbourhoods splits the test function into finitely many localized pieces (used to glue the local vorticity estimates in lem:vorticity-top-extension).

theorem ESS.vorticityGlue_integrableOn_mul {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {f h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f D MeasureTheory.volume) (hh : Continuous h) (hhc : HasCompactSupport h) (hhD : tsupport h ⊆ D) : MeasureTheory.IntegrableOn (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => f y * h y) D MeasureTheory.volume

The product of a locally integrable function with a continuous compactly supported function whose support lies in the open set is integrable there.

theorem ESS.vorticityGlue_generic {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f D MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g D MeasureTheory.volume) (L : (CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hLc : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → Continuous (L ψ)) (hLsupp : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), tsupport (L ψ) ⊆ tsupport ψ) (hLsum : ∀ (ι : Type) (s : Finset ι) (φ : ι → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (k : ι), ContDiff ℝ (↑⊤) (φ k)) → (L fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ k ∈ s, φ k z) = fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ k ∈ s, L (φ k) z) (hloc : ∀ z ∈ D, ∃ (N : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)), IsOpen N ∧ z ∈ N ∧ ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ N → tsupport ψ ⊆ D → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, f y * L ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, g y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ D → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, f y * L ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, g y * ψ y

A weak derivative identity for an abstract linear derivative of the test function, glued from neighbourhoods of the points of an open set.

theorem ESS.vorticityGlue_spatialPartial_sum {ι : Type} (s : Finset ι) (φ : ι → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hφ : ∀ (k : ι), ContDiff ℝ (↑⊤) (φ k)) (j : Fin 3) : (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ k ∈ s, φ k y) j z) = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ k ∈ s, CKN.spatialPartial (φ k) j z

The spatial partial derivative of a finite sum of smooth functions.

theorem ESS.vorticityGlue_timePartial_sum {ι : Type} (s : Finset ι) (φ : ι → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hφ : ∀ (k : ι), ContDiff ℝ (↑⊤) (φ k)) : (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ k ∈ s, φ k y) z) = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ k ∈ s, CKN.timePartial (φ k) z

The time partial derivative of a finite sum of smooth functions.

theorem ESS.vorticity_weak_glue_spatial {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f D MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g D MeasureTheory.volume) (j : Fin 3) (hloc : ∀ z ∈ D, ∃ (N : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)), IsOpen N ∧ z ∈ N ∧ ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ N → tsupport ψ ⊆ D → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, f y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, g y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ D → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, f y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, g y * ψ y

Gluing of weak derivative identities from local neighbourhoods.

theorem ESS.vorticity_weak_glue_time {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f D MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g D MeasureTheory.volume) (hloc : ∀ z ∈ D, ∃ (N : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)), IsOpen N ∧ z ∈ N ∧ ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ N → tsupport ψ ⊆ D → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, f y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, g y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ D → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, f y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in D, g y * ψ y

Gluing of weak time derivative identities from local neighbourhoods.