Countable full-pairing configurations for R-324

A full pairing on the doubled 2m carrier has exactly m covariance pairs. This file reindexes its dependent Fourier-assignment type by Fin m → ℤ⁴, then by ℕ when m > 0. It also defines the signed Euclidean increments whose sum is the external shift on every nonzero integrated configuration.

theorem Anderson4D.SmoothCutoff.r324FullPairCardEq {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : {i ∈ (↑κ).pairSupport | i < ↑κ i}.card = m

A full pairing of the doubled carrier has exactly m lower pair representatives.

def Anderson4D.SmoothCutoff.r324FullPairIndexEquiv {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : Fin m ≃ Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card

Canonical cast between the standard Fin m pair index and the dependent lower-endpoint enumeration.

Equations

• Anderson4D.SmoothCutoff.r324FullPairIndexEquiv κ = (Fin.castOrderIso ⋯).toEquiv

def Anderson4D.SmoothCutoff.r324FullConfigurationOfStandard {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4

Transport a standard m-tuple of lattice modes to the dependent assignment type of the covariance expansion.

Equations

• Anderson4D.SmoothCutoff.r324FullConfigurationOfStandard κ q = q ∘ ⇑(Anderson4D.SmoothCutoff.r324FullPairIndexEquiv κ).symm

def Anderson4D.SmoothCutoff.r324FullConfigurationEquiv {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : (Fin m → Z4) ≃ (Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4)

Exact equivalence between standard and dependent full-pairing configurations.

Equations

• Anderson4D.SmoothCutoff.r324FullConfigurationEquiv κ = (Anderson4D.SmoothCutoff.r324FullPairIndexEquiv κ).arrowCongr (Equiv.refl Anderson4D.Z4)

@[simp]

theorem Anderson4D.SmoothCutoff.r324FullConfigurationEquiv_apply {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : (r324FullConfigurationEquiv κ) q = r324FullConfigurationOfStandard κ q

Signed Euclidean increments

def Anderson4D.SmoothCutoff.z4EuclideanFrequencyAddHom : Z4 →+ EuclideanSpace ℝ (Fin dim)

The lattice-to-Euclidean frequency map as an additive homomorphism.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324StandardPairIncrement {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (i : Fin m) : EuclideanSpace ℝ (Fin dim)

One signed pair contribution, with sign reversed so that the total equals α+β rather than its negative.

Equations

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

theorem Anderson4D.SmoothCutoff.sum_r324StandardPairIncrement {m : ℕ} (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) : ∑ i : Fin m, r324StandardPairIncrement κ q i = z4EuclideanFrequency (-r324LeftModeSum (↑κ) (r324FullConfigurationOfStandard κ q))

The standard increments telescope to the negative signed left-mode sum before frequency conservation is imposed.

theorem Anderson4D.SmoothCutoff.sum_r324StandardPairIncrement_eq_external_of_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin m → Z4) (hne : ρ.r324FullPairingFourierIntegral ε α β κ (r324FullConfigurationOfStandard κ q) ≠ 0) : ∑ i : Fin m, r324StandardPairIncrement κ q i = z4EuclideanFrequency (α + β)

On a nonzero integrated configuration, the increments sum exactly to the external Fourier shift.

Natural-number enumeration

def Anderson4D.SmoothCutoff.r324NatEquivStandardConfigurations {m : ℕ} (hm : 0 < m) : ℕ ≃ (Fin m → Z4)

For m > 0, the standard configuration type is denumerable.

Equations

• Anderson4D.SmoothCutoff.r324NatEquivStandardConfigurations hm = (Denumerable.eqv (Fin m → Anderson4D.Z4)).symm

noncomputable def Anderson4D.SmoothCutoff.r324NatFullPairingFourierTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) : ℂ

The a-th integrated Fourier configuration of one full pairing.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324NatFullPairingIncrement {m : ℕ} (hm : 0 < m) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) (i : Fin m) : EuclideanSpace ℝ (Fin dim)

The Euclidean increments attached to the a-th natural-number configuration.

Equations

• Anderson4D.SmoothCutoff.r324NatFullPairingIncrement hm κ a i = Anderson4D.SmoothCutoff.r324StandardPairIncrement κ ((Anderson4D.SmoothCutoff.r324NatEquivStandardConfigurations hm) a) i

theorem Anderson4D.SmoothCutoff.summable_r324NatFullPairingFourierTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : Summable (ρ.r324NatFullPairingFourierTerm hm ε α β κ)

The natural-number configuration series is summable.

theorem Anderson4D.SmoothCutoff.integral_momentFullPairingPhysicalIntegrand_eq_nat_tsum (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : ∫ (p : R324PhysicalPoint m), r324Flatten (momentFullPairingPhysicalIntegrand ρ ε m α β κ) p ∂r324PhysicalMeasure m = ∑' (a : ℕ), ρ.r324NatFullPairingFourierTerm hm ε α β κ a

Exact natural-number tsum representation of one full-pairing physical integral.

theorem Anderson4D.SmoothCutoff.sum_r324NatFullPairingIncrement_eq_external_of_ne_zero (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (a : ℕ) (hne : ρ.r324NatFullPairingFourierTerm hm ε α β κ a ≠ 0) : ∑ i : Fin m, r324NatFullPairingIncrement hm κ a i = z4EuclideanFrequency (α + β)

Every nonzero natural-number configuration has the exact external increment sum.