Concrete data required of compact solenoidal velocity truncations. The actual radial-potential construction supplies this record separately.

structure Euler.ComparatorBridge.FiniteEnergyTruncationFamily (v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space) : Type

A family of smooth bounded truncations on a fixed unit time interval, with uniform kinetic energy and agreement inside the prescribed radius.

• coefficient : ℝ → SmoothTimeField (↑(Set.Icc 0 1)) EulerSmoothLimit.Space EulerSmoothLimit.Space

  Coefficient of FiniteEnergyTruncationFamily, of type `ℝ → SmoothTimeField (Icc (0 : ℝ)

  1. Space Space`.
• energy : ℝ

  Energy of FiniteEnergyTruncationFamily, of type ℝ.

• divergence (R : ℝ) : 0 < R → ∀ (t : ↑(Set.Icc 0 1)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (⇑((self.coefficient R).field t)) x = 0
• memLp (R : ℝ) : 0 < R → ∀ (t : ↑(Set.Icc 0 1)), MeasureTheory.MemLp (⇑((self.coefficient R).field t)) 2 MeasureTheory.volume
• energy_bound (R : ℝ) : 0 < R → ∀ (t : ↑(Set.Icc 0 1)), ∫ (x : EulerSmoothLimit.Space), ‖((self.coefficient R).field t) x‖ ^ 2 ≤ self.energy
• agrees (R : ℝ) : 0 < R → ∀ (t : ↑(Set.Icc 0 1)) (x : EulerSmoothLimit.Space), ‖x‖ < R → ((self.coefficient R).field t) x = v x ↑t