Natural-number covariance configurations for one full pairing

This small module packages the two configuration equivalences behind opaque natural-number terms. Downstream finite-fibre arguments can use the resulting shallow declarations without repeatedly elaborating the dependent Fourier-assignment type.

noncomputable def Anderson4D.SmoothCutoff.r324NatCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (κ : R324FullPairingIndex m) (a : ℕ) (v : Fin (2 * m) → T4) : ℂ

The a-th pointwise covariance Fourier configuration of one full pairing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.SmoothCutoff.r324NatCovarianceConfigurationWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (κ : R324FullPairingIndex m) (a : ℕ) : ℝ

Coordinate-independent norm weight of the preceding natural configuration.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.SmoothCutoff.norm_r324NatCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (κ : R324FullPairingIndex m) (a : ℕ) (v : Fin (2 * m) → T4) : ‖ρ.r324NatCovarianceConfigurationTerm hm ε κ a v‖ = ρ.r324NatCovarianceConfigurationWeight hm ε κ a

theorem Anderson4D.SmoothCutoff.summable_r324StandardCovarianceConfigurationWeight (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : R324FullPairingIndex m) : Summable fun (q : Fin m → Z4) => ρ.r324CovarianceConfigurationWeight ε (↑κ) (r324FullConfigurationOfStandard κ q)

Standardized configuration weights remain summable.

theorem Anderson4D.SmoothCutoff.summable_r324NatCovarianceConfigurationWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (κ : R324FullPairingIndex m) : Summable (ρ.r324NatCovarianceConfigurationWeight hm ε κ)

Natural-number covariance weights remain summable.

theorem Anderson4D.SmoothCutoff.summable_norm_r324NatCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (κ : R324FullPairingIndex m) (v : Fin (2 * m) → T4) : Summable fun (a : ℕ) => ‖ρ.r324NatCovarianceConfigurationTerm hm ε κ a v‖

theorem Anderson4D.SmoothCutoff.summable_r324NatCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (κ : R324FullPairingIndex m) (v : Fin (2 * m) → T4) : Summable fun (x : ℕ) => ρ.r324NatCovarianceConfigurationTerm hm ε κ x v

theorem Anderson4D.SmoothCutoff.tsum_r324NatCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (κ : R324FullPairingIndex m) (v : Fin (2 * m) → T4) : ∑' (a : ℕ), ρ.r324NatCovarianceConfigurationTerm hm ε κ a v = ↑(primitiveCovarianceProduct ρ ε m (↑κ) v)

The natural series is the complete covariance product of the full pairing.

noncomputable def Anderson4D.SmoothCutoff.r324NatCovarianceIncrementKey {m : ℕ} (hm : 0 < m) (κ : R324FullPairingIndex m) (a : ℕ) : Fin m → Z4

Signed left-increment key of the a-th natural configuration.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Anderson4D.SmoothCutoff.z4EuclideanFrequency_r324NatCovarianceIncrementKey {m : ℕ} (hm : 0 < m) (κ : R324FullPairingIndex m) (a : ℕ) (i : Fin m) : z4EuclideanFrequency (r324NatCovarianceIncrementKey hm κ a i) = r324NatFullPairingIncrement hm κ a i