Relative energy from cross testing #

The a.e. energy equality of the distinguished field combines with the competitor's energy inequality and the relative cross identity to give the integral inequality used in Gronwall's lemma.

source

noncomputable def ESS.lpsComparisonDistanceSq (u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) :

ℝ

The squared distance of two velocity slices.

Equations

ESS.lpsComparisonDistanceSq u v t = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, (v (x, t) k - u (x, t) k) ^ 2

Instances For

source

def ESS.lpsRelativeConvection (u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

ℝ

The relative convection density for two velocity fields and their specified gradients.

Equations

ESS.lpsRelativeConvection u v Du Dv z = ∑ k : Fin 3, u z k * ∑ j : Fin 3, (v z j - u z j) * (Dv z k j - Du z k j)

Instances For

source

def ESS.lpsRelativeGradientSq (Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

ℝ

The squared difference of two specified gradients.

Equations

ESS.lpsRelativeGradientSq Du Dv z = ∑ k : Fin 3, ∑ j : Fin 3, (Dv z k j - Du z k j) ^ 2

Instances For

source

theorem ESS.lps_relative_gradient_expansion {T : ℝ} {a b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T b v Dv pv) :

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), lpsRelativeGradientSq Du Dv z = ((∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv z k j * Dv z k j) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Dv z k j) + ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Du z k j

The squared gradient difference expands into the two dissipation terms and their cross pairing on every time slab.

source

theorem ESS.lps_relative_convection_bound_integrated {T K : ℝ} {u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {m : ℝ → ℝ} (hSliceBound : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRelativeConvection u v Du Dv (x, τ) ≤ (1 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRelativeGradientSq Du Dv (x, τ)) + K * (m τ * lpsComparisonDistanceSq u v τ)) (hC : MeasureTheory.Integrable (lpsRelativeConvection u v Du Dv) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hD : MeasureTheory.Integrable (lpsRelativeGradientSq Du Dv) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hmE : MeasureTheory.IntegrableOn (fun (τ : ℝ) => m τ * lpsComparisonDistanceSq u v τ) (Set.Ioo 0 T) MeasureTheory.volume) :

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), lpsRelativeConvection u v Du Dv z ≤ (1 / 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), lpsRelativeGradientSq Du Dv z) + K * ∫ (τ : ℝ) in 0..t, m τ * lpsComparisonDistanceSq u v τ

A fixed-time relative-convection estimate integrates to its space-time counterpart on almost every initial slab.

source

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t ≤ 2 * K * ∫ (τ : ℝ) in 0..t, m τ * lpsComparisonDistanceSq u v τ

A relative cross identity, the distinguished energy equality, the competitor energy inequality, and an integrated relative-convection bound imply the comparison inequality at almost every time. The energy equality is an explicit hypothesis so it can be supplied by lps_serrin_energy_equality.

source

theorem ESS.lps_relative_energy_grow_zero {T K : ℝ} {u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {m : ℝ → ℝ} (hT : 0 < T) (hK : 0 ≤ K) (hm : MeasureTheory.IntegrableOn m (Set.Ioo 0 T) MeasureTheory.volume) (hmNonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ m t) (hENonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ lpsComparisonDistanceSq u v t) (hmE : MeasureTheory.IntegrableOn (fun (t : ℝ) => m t * lpsComparisonDistanceSq u v t) (Set.Ioo 0 T) MeasureTheory.volume) (hmENonneg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ m t * lpsComparisonDistanceSq u v t) (hineq : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t ≤ 2 * K * ∫ (s : ℝ) in 0..t, m s * lpsComparisonDistanceSq u v s) :

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t = 0

The relative-energy inequality implies uniqueness when its coefficient and energy product satisfy the hypotheses of integral Gronwall.

source

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t = 0

The distinguished energy equality and the relative cross-testing inputs imply that the two weak fields agree almost everywhere.

source

∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t = 0

Fixed-time comparison bounds, the relative cross identity, and the distinguished energy equality imply almost-everywhere uniqueness.

Documentation

LeanPool.EscauriazaSereginSverak.LPS.RelativeEnergyAssembly

Relative energy from cross testing #