The weak local heat gain

A square-integrable distributional solution of the heat equation with a square-integrable divergence-form source on a space-time box has a square-integrable weak spatial gradient on every smaller box with the same top, with a bound by the data (the gradient part of lem:localized-vorticity-energy and lem:local-heat-gain). The gradient is the L² limit of the gradients of backward mollifications, which solve the equation pointwise up to the top.

theorem ESS.vorticityBox_isBounded (x₀ : CKN.Foundation.Parabolic.Vec3) (R : ℝ) (I : Set ℝ) (hI : Bornology.IsBounded I) : Bornology.IsBounded (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ I)

Space-time boxes over Euclidean balls are bounded.

theorem ESS.vorticityBox_isOpen (x₀ : CKN.Foundation.Parabolic.Vec3) (R a b : ℝ) : IsOpen (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b)

Space-time boxes over Euclidean balls with open time intervals are open.

theorem ESS.vorticity_integrableOn_of_memLp_box {x₀ : CKN.Foundation.Parabolic.Vec3} {R a b : ℝ} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b))) : MeasureTheory.IntegrableOn f (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b) MeasureTheory.volume

A square-integrable function on a bounded box is integrable there.

theorem ESS.vorticity_engine_radii {ε₀ : ℝ} (hε₀ : 0 < ε₀) : ∃ (ε : ℕ → ℝ), (∀ (n : ℕ), 0 < ε n) ∧ Filter.Tendsto ε Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), ε n ≤ ε₀

The shrinking radii of the backward mollifications used in the engines.

theorem ESS.vorticity_tendsto_prod_add {a b : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) (hb : Filter.Tendsto b Filter.atTop (nhds 0)) : Filter.Tendsto (fun (p : ℕ × ℕ) => a p.1 + b p.2) Filter.atTop (nhds 0)

A double sequence of sums of null sequences is null along the product filter.

theorem ESS.vorticityHeatEngine {r R κ : ℝ} (hr : 0 < r) (hrR : r < R) (hκ : 0 < κ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a b : ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (F : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), a + κ < b → b ≤ a + 1 → MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b)) → (∀ (j : Fin 3), MeasureTheory.MemLp (F j) 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, w y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, ∑ j : Fin 3, F j y * CKN.spatialPartial ψ j y) → ∃ (G : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (j : Fin 3), MeasureTheory.MemLp (G j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b))) ∧ (∀ (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, w y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b, G j y * ψ y) ∧ ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b, ∑ j : Fin 3, G j y ^ 2 ≤ C * ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, w y ^ 2 + ∑ j : Fin 3, F j y ^ 2

The weak local heat gain: a square-integrable distributional solution of ∂ₜ w - Δ w = div F with square-integrable F on a box has a square-integrable weak spatial gradient on every smaller box with the same top, bounded by the data (lem:localized-vorticity-energy, lem:local-heat-gain).