PrincipalResponseShellAverage

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the averaged fresh shell (h)_{z + cu_n}

Source displays in ABK26:

• names the fresh shell h := k_m - k_{m-h}, the increment of the infrared cutoff between the two scales of l.approximate.recurrence.formula;
• Step 3 of that lemma never uses h itself but only its average (h)_{z+cu_n} over the localization cube, which is the matrix conjugated away by the doubled shear bfG_{-(h)_{z+cu_n}} of e.Gh.def.

This module defines that average as a single Mat d and proves the one property the gauge algebra needs of it: it is antisymmetric.

Why it is skew

The standing assumption a.shell.antisymmetry is carried structurally, not as a hypothesis: the frozen carrier Algsuperdiff.Frozen.Assumptions.ShellField bundles forall x i j, j x i j = - j x j i into the type of a shell, so every finite increment k_m - k_{m-h} is a pointwise antisymmetric matrix field (Algsuperdiff.Section3.Cutoff.finiteShellIncrement_skew), and averaging over a cube is entrywise linear. Consequently freshShellCubeAverage_skew is unconditional -- no integrability, no measurability, and no event.

The antisymmetry consumed here is the separate standing node a.shell.antisymmetry.)

Carriers

• the localization cube is a free TriadicCube d argument R.
• the two scales are free integers lowScale <= highScale; in Step 3 they are m - h and m.
• the sample is a bare Cutoff.ShellSeq d, so that the definition is available before any lower-tail restriction. The two identification lemmas below, which need the lower-infinite cutoff, are stated on Cutoff.CutoffSample d.

Main results

• freshShellCubeAverage, freshShellCubeAverage_apply
• freshShellCubeAverage_skew -- the input required by CoarseGaugeCoeffField, CoarseGaugeResponse and CoarseGaugeCoarseMatrices, all of which are stated for a constant hbar with matTranspose hbar = -hbar
• freshShellCubeAverage_eq_cubeAverageMat_cutoff_sub and ..._coefficientCutoff_sub -- the identification of this matrix with the manuscript's (k_m - k_{m-h})_{z+cu_n} and with the average of the coefficient-field difference a_m - a_{m-h}.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.freshShellCubeAverage {d : ℕ} (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) : HCPolySupport.Mat d

The averaged fresh shell (h)_{z+cu_n} of ABK26 Step 3.

With h = k_{highScale} - k_{lowScale} the fresh shell and R the localization cube, this is the constant matrix (h)_R, entrywise the cube average of the finite shell increment.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.freshShellCubeAverage_apply {d : ℕ} (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (i j : Fin d) : freshShellCubeAverage R omega lowScale highScale i j = HCPolySupport.cubeAverage R fun (x : HCPolySupport.Vec d) => (Cutoff.finiteShellIncrement omega lowScale highScale).toFun x i j

Entrywise formula for the averaged fresh shell.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.freshShellCubeAverage_skew {d : ℕ} (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) : HCPolySupport.matTranspose (freshShellCubeAverage R omega lowScale highScale) = -freshShellCubeAverage R omega lowScale highScale

The averaged fresh shell is antisymmetric.

This is the hypothesis matTranspose hbar = -hbar of every declaration of CoarseGaugeCoeffField, CoarseGaugeResponse and CoarseGaugeCoarseMatrices, discharged at the carrier ABK26 Step 3 actually conjugates by.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.freshShellCubeAverage_eq_cubeAverageMat_cutoff_sub {d : ℕ} (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) {lowScale highScale : ℤ} (hle : lowScale ≤ highScale) : freshShellCubeAverage R (↑omega) lowScale highScale = HCPolySupport.cubeAverageMat R fun (x : HCPolySupport.Vec d) => (Cutoff.cutoff highScale omega).toFun x - (Cutoff.cutoff lowScale omega).toFun x

The identification with (k_m - k_{m-h})_{z+cu_n}. On the lower-tail carrier the finite increment is the difference of the two lower-infinite cutoffs, so the definition above is literally the manuscript's average of the fresh shell.