Fourier expansion of a residual-refined R-324 core

For one realized residual schedule, the primitive-pairing fibre remains inside the core. We first enumerate its finite contraction fibre times the absolutely convergent covariance configurations. We then group that series by the common Fin m → ℤ⁴ vector of signed left-translation increments. Thus every final grouped term has one shared increment list, while the primitive fibre sum is formed before taking a norm.

Enumerating one finite refined fibre times its configurations

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324RefinedContractionIndex {m : ℕ} (p : R324RefinedScheduleIndex m) : Type

Equations

• Anderson4D.SmoothCutoff.R324RefinedContractionIndex p = ↥(Anderson4D.momentRefinedContractionFiber m ↑p.fst ↑p.snd)

theorem Anderson4D.SmoothCutoff.r324RefinedContractionIndex_nonempty {m : ℕ} (p : R324RefinedScheduleIndex m) : Nonempty (R324RefinedContractionIndex p)

noncomputable def Anderson4D.SmoothCutoff.r324NatEquivRefinedContractionConfigurations {m : ℕ} (p : R324RefinedScheduleIndex m) : ℕ ≃ R324RefinedContractionIndex p × ℕ

Natural enumeration of a refined contraction entity together with one natural-number covariance configuration.

Equations

• Anderson4D.SmoothCutoff.r324NatEquivRefinedContractionConfigurations p = (Denumerable.eqv (Anderson4D.SmoothCutoff.R324RefinedContractionIndex p × ℕ)).symm

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

One raw covariance Fourier configuration in a refined fibre.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawIncrementKey {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (a : ℕ) : Fin m → Z4

Shared lattice increment key of a raw refined configuration.

Equations

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

@[simp]

theorem Anderson4D.SmoothCutoff.z4EuclideanFrequency_r324RefinedRawIncrementKey {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (a : ℕ) (i : Fin m) : z4EuclideanFrequency (r324RefinedRawIncrementKey hm p a i) = have u := (r324NatEquivRefinedContractionConfigurations p) a; have κ := (momentContractionEquivFullPairing m) ↑u.1; r324NatFullPairingIncrement hm κ u.2 i

theorem Anderson4D.SmoothCutoff.summable_norm_r324RefinedRawCovarianceConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : Summable fun (a : ℕ) => ‖ρ.r324RefinedRawCovarianceConfiguration hm ε p a v‖

theorem Anderson4D.SmoothCutoff.summable_r324RefinedRawCovarianceConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : Summable fun (x : ℕ) => ρ.r324RefinedRawCovarianceConfiguration hm ε p x v

theorem Anderson4D.SmoothCutoff.tsum_r324RefinedRawCovarianceConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : ∑' (a : ℕ), ρ.r324RefinedRawCovarianceConfiguration hm ε p a v = ∑ e ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd, ↑(primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v)

The raw natural series is exactly the covariance-product sum of the whole refined contraction fibre.

General summable grouping by a shared key

noncomputable def Anderson4D.SmoothCutoff.tsumByKey {A : Type u_1} {K : Type u_2} [AddCommMonoid A] [TopologicalSpace A] (f : ℕ → A) (key : ℕ → K) (k : K) : A

Fibrewise tsum of a summable series under an arbitrary key map.

Equations

• Anderson4D.SmoothCutoff.tsumByKey f key k = ∑' (a : { a : ℕ // key a = k }), f ↑a

theorem Anderson4D.SmoothCutoff.summable_tsumByKey {A : Type u_1} {K : Type u_2} [NormedAddCommGroup A] [CompleteSpace A] (f : ℕ → A) (key : ℕ → K) (hf : Summable f) : Summable (tsumByKey f key)

theorem Anderson4D.SmoothCutoff.tsum_tsumByKey {A : Type u_1} {K : Type u_2} [NormedAddCommGroup A] [CompleteSpace A] (f : ℕ → A) (key : ℕ → K) (hf : Summable f) : ∑' (k : K), tsumByKey f key k = ∑' (a : ℕ), f a

Increment-key grouped refined cores

noncomputable def Anderson4D.SmoothCutoff.r324KeyGroupedCovarianceConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ℂ

Covariance configurations in a refined fibre, grouped by a common signed left-increment vector.

Equations

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

theorem Anderson4D.SmoothCutoff.summable_r324KeyGroupedCovarianceConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : Summable fun (b : ℕ) => ρ.r324KeyGroupedCovarianceConfiguration hm ε p b v

theorem Anderson4D.SmoothCutoff.tsum_r324KeyGroupedCovarianceConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : ∑' (b : ℕ), ρ.r324KeyGroupedCovarianceConfiguration hm ε p b v = ∑ e ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd, ↑(primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v)

noncomputable def Anderson4D.SmoothCutoff.r324KeyGroupedRefinedEndpointCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ℂ

Full grouped internal core: the common interior Green factors times the covariance configurations sharing one increment vector.

Equations

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

theorem Anderson4D.SmoothCutoff.summable_r324KeyGroupedRefinedEndpointCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : Summable fun (b : ℕ) => ρ.r324KeyGroupedRefinedEndpointCore hm ε p b v

theorem Anderson4D.SmoothCutoff.tsum_r324KeyGroupedRefinedEndpointCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : ∑' (b : ℕ), ρ.r324KeyGroupedRefinedEndpointCore hm ε p b v = r324RefinedEndpointCore ρ ε m (↑p.fst) (↑p.snd) (r324RefinedScheduleRepresentative p) v