The actual source outer cutoff in rescaled particle labels.

noncomputable def EulerMeanBoundary.scaledCutoff (ℓ : ℝ) (hℓ : 0 < ℓ) : Cutoff

Scaled cutoff, bundling field, smooth, compact.

Equations

• EulerMeanBoundary.scaledCutoff ℓ hℓ = { field := fun (x : EulerSmoothLimit.Space) => EulerSpatialCutoffs.outerCutoff (ℓ • x), smooth := ⋯, compact := ⋯ }

theorem EulerMeanBoundary.scaledCutoff_one (ℓ : ℝ) (hℓ : 0 < ℓ) (x : EulerSmoothLimit.Space) (hx : ‖ℓ • x‖ ≤ 1) : (scaledCutoff ℓ hℓ).field x = 1

theorem EulerMeanBoundary.scaledCutoff_one_on_ball (ℓ : ℝ) (hℓ : 0 < ℓ) (x : EulerSmoothLimit.Space) : x ∈ Metric.ball 0 ℓ⁻¹ → (scaledCutoff ℓ hℓ).field x = 1

theorem EulerMeanBoundary.scaledCutoff_support (ℓ : ℝ) (hℓ : 0 < ℓ) : tsupport (scaledCutoff ℓ hℓ).field ⊆ {x : EulerSmoothLimit.Space | ‖ℓ • x‖ ≤ 2}

theorem EulerMeanBoundary.scaledCutoff_even (ℓ : ℝ) (hℓ : 0 < ℓ) (x : EulerSmoothLimit.Space) : (scaledCutoff ℓ hℓ).field (-x) = (scaledCutoff ℓ hℓ).field x

theorem EulerMeanBoundary.physical_ball_eq (ℓ r : ℝ) (hℓ : 0 < ℓ) : {x : EulerSmoothLimit.Space | ‖ℓ • x‖ < r} = Metric.ball 0 (ℓ⁻¹ * r)

theorem EulerMeanBoundary.scaledCutoff_gevrey (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (scaledCutoff ℓ hℓ).field x‖ ≤ (9 * (1 + 3 / EulerGevreyCutoff.bumpMass) ^ 2) ^ 3 * EulerGevrey.majorant 256 0 n

Rescaling by at most one preserves the fixed factorial derivative bound.