Explicit finite-dimensional norm comparisons for the actual H³ energy.

noncomputable def EulerOrdinarySobolev.tensorNorm (s : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Tensor norm, given by ∑ n ∈ range (s+1), ‖A.jetLp n‖.

Equations

• EulerOrdinarySobolev.tensorNorm s A = ∑ n ∈ Finset.range (s + 1), ‖A.jetLp n‖

theorem EulerOrdinarySobolev.tensorNorm_eq (s : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : tensorNorm s A = EulerSmoothSobolev.realTensorSobolevNorm 3 s A.field

theorem EulerOrdinarySobolev.tensorNorm_nonneg (s : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : 0 ≤ tensorNorm s A

theorem EulerOrdinarySobolev.wordBound_tensorNorm (s : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : WordBound s (tensorNorm s A) A

theorem EulerOrdinarySobolev.tensorNorm_three_le (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M : ℝ) (hA : WordBound 3 M A) : tensorNorm 3 A ≤ 40 * M

theorem EulerOrdinarySobolev.tensorNorm_le_sqrt_energy (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : tensorNorm 3 A ≤ 40 * √(wordEnergy 3 A)

theorem EulerOrdinarySobolev.energy_le_tensorNorm_sq (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : wordEnergy 3 A ≤ 40 * tensorNorm 3 A ^ 2

theorem EulerOrdinarySobolev.sqrt_energy_le_tensorNorm (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : √(wordEnergy 3 A) ≤ 7 * tensorNorm 3 A