Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.VorticityDivCurlEngine

The weak local div–curl recovery #

A square-integrable space-time vector field which is weakly divergence free and whose weak antisymmetric derivatives are square integrable has a square-integrable weak spatial gradient on every smaller box with the same top, bounded by the data (lem:local-div-curl, integrated in time). The gradient is the L² limit of the gradients of backward mollifications, to which the smooth estimate applies at every time.

source
theorem ESS.vorticity_setIntegral_prod_time_mono {B B' : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hI : MeasurableSet I) {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (B ×ˢ I) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (B' ×ˢ I) MeasureTheory.volume) (h : ∀ t ∈ I, ∫ (x : CKN.Foundation.Parabolic.Vec3) in B, f (x, t) ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3) in B', g (x, t)) :
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ I, f z ≤ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in B' ×ˢ I, g z

Integrating a time-sliced inequality over a time interval.

source
theorem ESS.vorticityDivCurl_integrated {r R₁ C₀ : ℝ} (hsmooth : ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (V : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ), (∀ (b : Fin 3), ContDiff ℝ (↑⊤) (V b)) → ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ r, ∑ a : Fin 3, ∑ b : Fin 3, CKN.spatialDeriv (V b) a x ^ 2 ≤ C₀ * ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ R₁, (∑ a : Fin 3, CKN.spatialDeriv (V a) a x) ^ 2 + ∑ a : Fin 3, ∑ b : Fin 3, (CKN.spatialDeriv (V b) a x - CKN.spatialDeriv (V a) b x) ^ 2 + ∑ b : Fin 3, V b x ^ 2) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₁ t₂ : ℝ) {V : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hV : ∀ (c : Fin 3), ContDiff ℝ (↑⊤) (V c)) {Φ : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hΦ : ∀ (a c : Fin 3), Continuous (Φ a c)) (hdiv : ∀ z ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R₁ ×ˢ Set.Ioo t₁ t₂, ∑ a : Fin 3, CKN.spatialPartial (V a) a z = 0) (hcurl : ∀ z ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R₁ ×ˢ Set.Ioo t₁ t₂, ∀ (a c : Fin 3), CKN.spatialPartial (V c) a z - CKN.spatialPartial (V a) c z = Φ a c z) :
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo t₁ t₂, ∑ a : Fin 3, ∑ c : Fin 3, CKN.spatialPartial (V c) a z ^ 2 ≤ C₀ * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R₁ ×ˢ Set.Ioo t₁ t₂, ∑ a : Fin 3, ∑ c : Fin 3, Φ a c z ^ 2 + ∑ c : Fin 3, V c z ^ 2

The smooth div–curl estimate integrated over a time interval, for smooth fields whose divergence vanishes and whose antisymmetric derivatives are prescribed on the outer box.

source
theorem ESS.vorticityDivCurlEngine {r R κ : ℝ} (hr : 0 < r) (hrR : r < R) (hκ : 0 < κ) :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a b : ℝ) (Y : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Ω : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), MeasureTheory.MemLp (Y i) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b))) → (∀ (i k : Fin 3), MeasureTheory.MemLp (Ω i k) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b))) → (∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, ∑ i : Fin 3, Y i y * CKN.spatialPartial ψ i y = 0) → (∀ (i k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, Y k y * CKN.spatialPartial ψ i y - Y i y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, Ω i k y * ψ y) → ∃ (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b))) ∧ (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b, Y i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b, G i j y * ψ y) ∧ ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b, ∑ i : Fin 3, ∑ j : Fin 3, G i j y ^ 2 ≤ C * ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, ∑ i : Fin 3, ∑ k : Fin 3, Ω i k y ^ 2 + ∑ i : Fin 3, Y i y ^ 2

The weak local div–curl recovery on boxes (lem:local-div-curl, integrated in time).