The energy estimate for each spatial derivative of the cutoff solution #
Each spatial derivative ∂^β w, |β| ≤ m, of the cutoff solution solves the
heat equation on ℝ³ × (a, b) with a square-integrable source: H itself for
β = [], and the divergence-form source ∂_k (∂^{β'} H) for
β = β' ++ [k]. It vanishes near t = a, so the energy estimate of
lem:localized-vorticity-energy (vlHeat_energy) gives a curve continuous in
L² and a square-integrable weak gradient, bounded by the data.
theorem
ESS.integral_slab_sq_eq
{a b : ℝ}
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
:
Slab integrals of squares as iterated integrals.
theorem
ESS.integrable_slab_sq_slices
{a b : ℝ}
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
:
MeasureTheory.Integrable (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), F (x, s) ^ 2)
(MeasureTheory.volume.restrict (Set.Ioo a b))
theorem
ESS.vlHeat_result
{a b : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(sol : CKN.VlHeatSolution a b w H f fun (x : CKN.Foundation.Parabolic.Vec3) => 0)
(M : ℝ)
(hM :
((∑ j : Fin 3, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, H j p ^ 2) + ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p ^ 2) + ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, f p ^ 2 ≤ M)
:
∃ (Zc : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (Dg :
Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
Continuous Zc ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (ht : t ∈ Set.Icc a b),
↑↑(Zc ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, t)) ∧ (∀ (j : Fin 3), MeasureTheory.MemLp (Dg j) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) ∧ (∀ (j : Fin 3), IsSpaceTimeWeakPartial (CKN.vlSlab a b) j w (Dg j)) ∧ ∀ (t : ↑(Set.Icc a b)),
‖Zc t‖ ^ 2 + ∑ j : Fin 3, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, Dg j p ^ 2 ≤ 2 * M
The output of the energy estimate, with the data energy bounded by M.
theorem
ESS.localHeatGain_wordEnergy
{m : ℕ}
(hm1 : 1 ≤ m)
{a b δ : ℝ}
(hab : a < b)
(hδ : 0 < δ)
{Dw DH : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hDw : IsSpaceTimeFamily m (CKN.vlSlab a b) Dw)
(hDH : IsSpaceTimeFamily (m - 1) (CKN.vlSlab a b) DH)
(hheat : CKN.IsHeatSolutionOn Set.univ (Set.Ioo a b) (Dw []) (DH []))
(hsm : ∀ (α : List (Fin 3)), MeasureTheory.StronglyMeasurable (Dw α))
(hsmH : ∀ (α : List (Fin 3)), MeasureTheory.StronglyMeasurable (DH α))
(hz0 : ∀ (α : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.2 < a + δ → Dw α p = 0)
(β : List (Fin 3))
(hβ : β ∈ CKN.sobolevWords m)
:
∃ (Zc : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (Dg :
Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
Continuous Zc ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (ht : t ∈ Set.Icc a b),
↑↑(Zc ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => Dw β (x, t)) ∧ (∀ (j : Fin 3), MeasureTheory.MemLp (Dg j) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) ∧ (∀ (j : Fin 3), IsSpaceTimeWeakPartial (CKN.vlSlab a b) j (Dw β) (Dg j)) ∧ ∀ (t : ↑(Set.Icc a b)),
‖Zc t‖ ^ 2 + ∑ j : Fin 3, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, Dg j p ^ 2 ≤ 2 * ((∑ α ∈ CKN.sobolevWords (m - 1),
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, DH α p ^ 2) + ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, Dw β p ^ 2)
The energy estimate for each spatial derivative of order at most m.