Analytic facts about the cutoff covariance

This file derives the elementary analytic input about the cutoff ρ and its Euclidean covariance η = ρ * ρ directly from SmoothCutoff. In particular, compact support is not carried as an extra hypothesis: it follows from the explicit support-radius field.

These lemmas are the analytic base used by the n = 1 case and by the cellwise estimates in paper §5.

theorem Anderson4D.SmoothCutoff.continuous (ρ : SmoothCutoff) : Continuous ρ.toFun

A smooth cutoff is continuous.

theorem Anderson4D.SmoothCutoff.hasCompactSupport (ρ : SmoothCutoff) : HasCompactSupport ρ.toFun

The explicit support-radius field implies compact support.

theorem Anderson4D.SmoothCutoff.integrable (ρ : SmoothCutoff) : MeasureTheory.Integrable ρ.toFun MeasureTheory.volume

Every smooth cutoff is Lebesgue-integrable.

theorem Anderson4D.SmoothCutoff.exists_pos_uniform_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : R4), ρ.toFun x ≤ C

A named positive pointwise bound for the cutoff.

theorem Anderson4D.SmoothCutoff.integrable_eta_integrand (ρ : SmoothCutoff) (x : R4) : MeasureTheory.Integrable (fun (y : R4) => ρ.toFun y * ρ.toFun (x - y)) MeasureTheory.volume

The convolution integrand defining η is integrable.

theorem Anderson4D.SmoothCutoff.eta_nonneg (ρ : SmoothCutoff) (x : R4) : 0 ≤ ρ.eta x

The Euclidean covariance is nonnegative.

theorem Anderson4D.SmoothCutoff.eta_le_of_bound (ρ : SmoothCutoff) {C : ℝ} (hC : ∀ (x : R4), ρ.toFun x ≤ C) (x : R4) : ρ.eta x ≤ C

The covariance is bounded uniformly by any pointwise cutoff bound.

theorem Anderson4D.SmoothCutoff.exists_pos_eta_uniform_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : R4), ρ.eta x ≤ C

Consequently η admits a positive global upper bound depending only on the named cutoff.