Dilation and local positivity of cutoff covariances

This file supplies the cutoff-dependent auxiliary covariance used by the relative-translation derivative route in paper §4.2. Dilating a cutoff preserves the frozen SmoothCutoff contract and gives an exact scaling law for η = ρ * ρ.

noncomputable def Anderson4D.SmoothCutoff.dilate (ρ : SmoothCutoff) (a : ℝ) (ha : 0 < a) : SmoothCutoff

Dilation by a positive scale, with the same normalization as rescale.

Equations

• ρ.dilate a ha = { toFun := ρ.rescale a, radius := a * ρ.radius, radius_pos := ⋯, smooth := ⋯, nonneg := ⋯, support_subset := ⋯, memE := ⋯, integral_one := ⋯ }

@[simp]

theorem Anderson4D.SmoothCutoff.dilate_apply (ρ : SmoothCutoff) (a : ℝ) (ha : 0 < a) (x : R4) : (ρ.dilate a ha).toFun x = a⁻¹ ^ dim * ρ.toFun (a⁻¹ • x)

@[simp]

theorem Anderson4D.SmoothCutoff.dilate_radius (ρ : SmoothCutoff) (a : ℝ) (ha : 0 < a) : (ρ.dilate a ha).radius = a * ρ.radius

theorem Anderson4D.SmoothCutoff.dilate_toFun_eq_rescale (ρ : SmoothCutoff) (a : ℝ) (ha : 0 < a) : (ρ.dilate a ha).toFun = ρ.rescale a

theorem Anderson4D.SmoothCutoff.eta_dilate (ρ : SmoothCutoff) (a : ℝ) (ha : 0 < a) (x : R4) : (ρ.dilate a ha).eta x = a⁻¹ ^ dim * ρ.eta (a⁻¹ • x)

The covariance of a dilated cutoff has the exact four-dimensional scaling dictated by convolution.

theorem Anderson4D.SmoothCutoff.contDiff_eta (ρ : SmoothCutoff) (n : ℕ) : ContDiff ℝ (↑n) ρ.eta

The cutoff covariance is smooth to every requested finite order.

theorem Anderson4D.SmoothCutoff.continuous_eta (ρ : SmoothCutoff) : Continuous ρ.eta

In particular, the cutoff covariance is continuous.

theorem Anderson4D.SmoothCutoff.hasCompactSupport_eta (ρ : SmoothCutoff) : HasCompactSupport ρ.eta

Convolution preserves compact support for the cutoff covariance.