Actual initial support in physical-label coordinates for the mean boundary operator.

theorem EulerMeanBoundary.scaledBoundary_zero_outside (ℓ : ℝ) (hℓ : 0 < ℓ) (z : ↥EulerMeanSolenoidal.L2) : ∀ᵐ (x : EulerSmoothLimit.Space), 2 < ‖ℓ • x‖ → ↑↑((boundaryOperator (scaledCutoff ℓ hℓ)) z) x = 0

theorem EulerMeanBoundary.scaledBoundary_multiple_zero_outside (ℓ : ℝ) (hℓ : 0 < ℓ) (L : ℝ) (z : ↥EulerMeanSolenoidal.L2) : ∀ᵐ (x : EulerSmoothLimit.Space), 2 < ‖ℓ • x‖ → ↑↑(L • (boundaryOperator (scaledCutoff ℓ hℓ)) z) x = 0

theorem EulerMeanBoundary.scaledBoundary_continuous_support (ℓ : ℝ) (hℓ : 0 < ℓ) (L : ℝ) (z : ↥EulerMeanSolenoidal.L2) (b : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hb : Continuous b) (hrep : b =ᵐ[MeasureTheory.volume] ↑↑(L • (boundaryOperator (scaledCutoff ℓ hℓ)) z)) : tsupport b ⊆ {x : EulerSmoothLimit.Space | ‖ℓ • x‖ ≤ 2}

Any continuous representative of the actual initial boundary velocity has this support.

theorem EulerMeanBoundary.scaledBoundary_continuous_compact (ℓ : ℝ) (hℓ : 0 < ℓ) (L : ℝ) (z : ↥EulerMeanSolenoidal.L2) (b : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hb : Continuous b) (hrep : b =ᵐ[MeasureTheory.volume] ↑↑(L • (boundaryOperator (scaledCutoff ℓ hℓ)) z)) : HasCompactSupport b