Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.VorticityWeakLinear

Linearity of weak spatial derivatives #

Weak spatial derivatives of sums, differences and negatives, used to differentiate the vorticity flux, a sum of products, in the bootstrap of thm:vorticity-regularity.

source
theorem ESS.vorticity_weakPartial_sub {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f₁ f₂ g₁ g₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {j : Fin 3} (hf₁ : MeasureTheory.IntegrableOn f₁ W MeasureTheory.volume) (hf₂ : MeasureTheory.IntegrableOn f₂ W MeasureTheory.volume) (hg₁ : MeasureTheory.IntegrableOn g₁ W MeasureTheory.volume) (hg₂ : MeasureTheory.IntegrableOn g₂ W MeasureTheory.volume) (h₁ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₁ y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₁ y * ψ y) (h₂ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₂ y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₂ y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) :
ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (f₁ y - f₂ y) * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (g₁ y - g₂ y) * ψ y

The weak derivative of a difference.

source
theorem ESS.vorticity_weakPartial_add {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f₁ f₂ g₁ g₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {j : Fin 3} (hf₁ : MeasureTheory.IntegrableOn f₁ W MeasureTheory.volume) (hf₂ : MeasureTheory.IntegrableOn f₂ W MeasureTheory.volume) (hg₁ : MeasureTheory.IntegrableOn g₁ W MeasureTheory.volume) (hg₂ : MeasureTheory.IntegrableOn g₂ W MeasureTheory.volume) (h₁ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₁ y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₁ y * ψ y) (h₂ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f₂ y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g₂ y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) :
ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (f₁ y + f₂ y) * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (g₁ y + g₂ y) * ψ y

The weak derivative of a sum.

source
theorem ESS.vorticity_weakPartial_neg {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {j : Fin 3} (h : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) :
ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, -f y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, -g y * ψ y

The weak derivative of a negative.