The energy inequality in the limit #
The kernel energy inequality for the mollifiers ρₙ, with Young's inequality
‖ρₙ ⋆ g‖₂ ≤ ‖g‖₂, gives a bound uniform in n. It passes to the limit
curve and to the limit gradient, which proves the energy estimate for weak
heat solutions with L² data (lem:localized-vorticity-energy).
noncomputable def
ESS.vlDataEnergy
(w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ)
(w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(a t : ℝ)
:
The energy of the data up to time t.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ESS.vlCurve_energy_le
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
(n : ℕ)
(t : ↑(Set.Icc a τ))
:
The uniform bound for the mollified curves and gradients.
theorem
ESS.vlGrad_sq_tendsto
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
(j : Fin 3)
(t : ↑(Set.Icc a τ))
:
Filter.Tendsto (fun (n : ℕ) => ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a ↑t, vlGrad w n j p ^ 2)
Filter.atTop (nhds (∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a ↑t, ↑↑(vlGradLimit sol j) p ^ 2))
The squared L² integral of the limit gradient on a shorter slab is the
limit of the mollified ones.
theorem
ESS.vlLimit_energy_le
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
(t : ↑(Set.Icc a τ))
:
‖vlLimit sol t‖ ^ 2 + ∑ j : Fin 3, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a ↑t, ↑↑(vlGradLimit sol j) p ^ 2 ≤ vlDataEnergy w₀ w H f a ↑t
The energy inequality for the limit.
theorem
ESS.vlHeat_energy
{a τ : ℝ}
{w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(sol : CKN.VlHeatSolution a τ w H f w₀)
:
∃ (Z : ↑(Set.Icc a τ) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (D :
Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
Continuous Z ∧ ↑↑(Z ⟨a, ⋯⟩) =ᵐ[MeasureTheory.volume] w₀ ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), ∀ (ht : t ∈ Set.Icc a τ),
↑↑(Z ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, t)) ∧ (∀ (j : Fin 3), MeasureTheory.MemLp (D j) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a τ))) ∧ (∀ (j : Fin 3),
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a τ),
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, w p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, D j p * φ p) ∧ ∀ (t : ↑(Set.Icc a τ)),
‖Z t‖ ^ 2 + ∑ j : Fin 3, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a ↑t, D j p ^ 2 ≤ vlDataEnergy w₀ w H f a ↑t
The energy estimate for a weak heat solution with square-integrable data
(lem:localized-vorticity-energy, one component).