Positive auxiliary cutoff covariance

The relative-translation derivative route needs a positive covariance majorant on the support of every derivative of the original covariance. This file constructs that majorant from a named, cutoff-dependent dilation.

Simultaneous Euclidean sign flips

def Anderson4D.flipR4Coords (s : Finset (Fin dim)) (x : R4) : R4

Negate precisely the Euclidean coordinates in s.

Equations

• Anderson4D.flipR4Coords s x i = if i ∈ s then -x i else x i

theorem Anderson4D.flipR4Coords_insert (s : Finset (Fin dim)) (i : Fin dim) (hi : i ∉ s) (x : R4) : flipR4Coords (insert i s) x = Function.update (flipR4Coords s x) i (-flipR4Coords s x i)

theorem Anderson4D.MemEClassR4.flipR4Coords_invariant {f : R4 → ℝ} (hf : MemEClassR4 f) (s : Finset (Fin dim)) (x : R4) : f (flipR4Coords s x) = f x

Membership in 𝓔 gives invariance under any set of Euclidean coordinate sign flips.

theorem Anderson4D.MemEClassR4.neg_invariant {f : R4 → ℝ} (hf : MemEClassR4 f) (x : R4) : f (-x) = f x

In particular, a cutoff in 𝓔 is invariant under total negation.

Strict positivity near the origin

theorem Anderson4D.SmoothCutoff.exists_cutoff_ne_zero (ρ : SmoothCutoff) : ∃ (x : R4), ρ.toFun x ≠ 0

A normalized nonnegative cutoff is nonzero somewhere.

theorem Anderson4D.SmoothCutoff.eta_zero_pos (ρ : SmoothCutoff) : 0 < ρ.eta 0

The autocorrelation covariance is strictly positive at the origin.

theorem Anderson4D.SmoothCutoff.exists_eta_pos_ball (ρ : SmoothCutoff) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (x : R4), ‖x‖ < δ → 0 < ρ.eta x

The cutoff covariance is strictly positive on a ball about zero.

Explicit support geometry

theorem Anderson4D.SmoothCutoff.support_eta_subset_ball_two_radius (ρ : SmoothCutoff) : Function.support ρ.eta ⊆ Metric.ball 0 (2 * ρ.radius)

Every nonzero covariance point lies in the open radius-2R ball.

theorem Anderson4D.SmoothCutoff.tsupport_eta_subset_closedBall_two_radius (ρ : SmoothCutoff) : tsupport ρ.eta ⊆ Metric.closedBall 0 (2 * ρ.radius)

The topological support of η lies in the corresponding closed ball.

A named cutoff-dependent positive majorant

noncomputable def Anderson4D.SmoothCutoff.etaPosRadius (ρ : SmoothCutoff) : ℝ

A chosen radius on which the original covariance is positive. This constant intentionally depends on ρ.

Equations

• ρ.etaPosRadius = Classical.choose ⋯

theorem Anderson4D.SmoothCutoff.etaPosRadius_pos (ρ : SmoothCutoff) : 0 < ρ.etaPosRadius

theorem Anderson4D.SmoothCutoff.eta_pos_of_norm_lt_etaPosRadius (ρ : SmoothCutoff) {x : R4} (hx : ‖x‖ < ρ.etaPosRadius) : 0 < ρ.eta x

noncomputable def Anderson4D.SmoothCutoff.auxiliaryScale (ρ : SmoothCutoff) : ℝ

A dilation large enough to make its covariance positive throughout the full topological support of the original covariance.

Equations

• ρ.auxiliaryScale = 4 * ρ.radius / ρ.etaPosRadius

theorem Anderson4D.SmoothCutoff.auxiliaryScale_pos (ρ : SmoothCutoff) : 0 < ρ.auxiliaryScale

noncomputable def Anderson4D.SmoothCutoff.auxiliaryCutoff (ρ : SmoothCutoff) : SmoothCutoff

The named auxiliary cutoff used in derivative majorants.

Equations

• ρ.auxiliaryCutoff = ρ.dilate ρ.auxiliaryScale ⋯

theorem Anderson4D.SmoothCutoff.auxiliaryScale_mul_etaPosRadius (ρ : SmoothCutoff) : ρ.auxiliaryScale * ρ.etaPosRadius = 4 * ρ.radius

theorem Anderson4D.SmoothCutoff.norm_inv_auxiliaryScale_smul_lt_etaPosRadius_of_mem_tsupport (ρ : SmoothCutoff) {x : R4} (hx : x ∈ tsupport ρ.eta) : ‖ρ.auxiliaryScale⁻¹ • x‖ < ρ.etaPosRadius

Points in tsupport η enter the positivity ball after the named auxiliary dilation.

theorem Anderson4D.SmoothCutoff.auxiliaryCutoff_eta_pos_on_tsupport (ρ : SmoothCutoff) {x : R4} (hx : x ∈ tsupport ρ.eta) : 0 < ρ.auxiliaryCutoff.eta x

The auxiliary covariance is strictly positive wherever any derivative of the original compactly supported covariance can be nonzero.