Common definitions for whole-space comparison

These are the ordinary volume energies and differential expressions. No comparison estimate or pressure representation is assumed in this module.

@[reducible, inline]

abbrev NavierStokesR3.Comparison.slab (a b : ℝ) : Set ProblemStatement.SpaceTime

Slab: an abbreviation for Icc a b ×ˢ univ.

Equations

• NavierStokesR3.Comparison.slab a b = Set.Icc a b ×ˢ Set.univ

@[reducible, inline]

noncomputable abbrev NavierStokesR3.Comparison.partialD {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i : Fin 3) (f : ProblemStatement.Space → E) (x : ProblemStatement.Space) : E

Partial D: an abbreviation for NavierStokes.SolutionDifference.spatialPartial i f x.

Equations

• NavierStokesR3.Comparison.partialD i f x = NavierStokes.SolutionDifference.spatialPartial i f x

noncomputable def NavierStokesR3.Comparison.comparisonLpNorm {E : Type u_1} [NormedAddCommGroup E] (p : ENNReal) (f : ProblemStatement.Space → E) : ℝ

Comparison Lᵖ norm, given by (eLpNorm f p (volume : Measure Space)).toReal.

Equations

• NavierStokesR3.Comparison.comparisonLpNorm p f = (MeasureTheory.eLpNorm f p MeasureTheory.volume).toReal

noncomputable def NavierStokesR3.Comparison.l2Sq {E : Type u_1} [NormedAddCommGroup E] (f : ProblemStatement.Space → E) : ℝ

L2 sq, given by ∫ x : Space, ‖f x‖ ^ 2.

Equations

• NavierStokesR3.Comparison.l2Sq f = ∫ (x : NavierStokesR3.ProblemStatement.Space), ‖f x‖ ^ 2

noncomputable def NavierStokesR3.Comparison.gradientSq (f : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ℝ

Gradient sq, given by ∑ i : Fin 3, ‖partialD i f x‖ ^ 2.

Equations

• NavierStokesR3.Comparison.gradientSq f x = ∑ i : Fin 3, ‖NavierStokesR3.Comparison.partialD i f x‖ ^ 2

noncomputable def NavierStokesR3.Comparison.weightedEnergy (χ : ProblemStatement.Space → ℝ) (w : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Weighted energy, given by ∫ x : Space, χ x * ‖w (t, x)‖ ^ 2.

Equations

• NavierStokesR3.Comparison.weightedEnergy χ w t = ∫ (x : NavierStokesR3.ProblemStatement.Space), χ x * ‖w (t, x)‖ ^ 2

noncomputable def NavierStokesR3.Comparison.weightedEnergyRate (χ : ProblemStatement.Space → ℝ) (w : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Weighted energy rate, given by ∫ x : Space, χ x * (2 * ⟪w (t, x), NavierStokes.ProblemStatement.temporalDerivative w t x⟫_ℝ).

Equations

• NavierStokesR3.Comparison.weightedEnergyRate χ w t = ∫ (x : NavierStokesR3.ProblemStatement.Space), χ x * (2 * inner ℝ (w (t, x)) (NavierStokes.ProblemStatement.temporalDerivative w t x))

noncomputable def NavierStokesR3.Comparison.weightedDissipation (χ : ProblemStatement.Space → ℝ) (w : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Weighted dissipation, given by ∫ x : Space, χ x * gradientSq (fun y => w (t, y)) x.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokesR3.Comparison.dissipationRoot (φ : ProblemStatement.Space → ℝ) (w : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Dissipation root, given by Real.sqrt (weightedDissipation (fun x => φ x ^ 8) w t).

Equations

• NavierStokesR3.Comparison.dissipationRoot φ w t = √(NavierStokesR3.Comparison.weightedDissipation (fun (x : NavierStokesR3.ProblemStatement.Space) => φ x ^ 8) w t)

noncomputable def NavierStokesR3.Comparison.cutoffL6 (φ : ProblemStatement.Space → ℝ) (w : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Cutoff L6, given by comparisonLpNorm 6 (fun x => (φ x ^ 4) • w (t, x)).

Equations

• NavierStokesR3.Comparison.cutoffL6 φ w t = NavierStokesR3.Comparison.comparisonLpNorm 6 fun (x : NavierStokesR3.ProblemStatement.Space) => φ x ^ 4 • w (t, x)

def NavierStokesR3.Comparison.tensorDiff (u v : ProblemStatement.VelocityField) (t : ℝ) (i j : Fin 3) (x : ProblemStatement.Space) : ℝ

Tensor diff, given by u (t, x) i * u (t, x) j - v (t, x) i * v (t, x) j.

Equations

• NavierStokesR3.Comparison.tensorDiff u v t i j x = (u (t, x)).ofLp i * (u (t, x)).ofLp j - (v (t, x)).ofLp i * (v (t, x)).ofLp j