Physical Green convolution and the Fourier-multiplier realization

The bounded Green operator on TorusL2 was defined spectrally. This file proves that on continuous inputs it agrees with convolution by the paper's heat-kernel Green function against paperMeasure. This is the analytic adapter needed to iterate physical parametrix kernels.

theorem Anderson4D.instPaperMeasureIsAddLeftInvariant : paperMeasure.IsAddLeftInvariant

theorem Anderson4D.instPaperMeasureIsAddRightInvariant : paperMeasure.IsAddRightInvariant

theorem Anderson4D.instPaperMeasureIsNegInvariant : paperMeasure.IsNegInvariant

theorem Anderson4D.charT4_add_apply (k : Z4) (x y : T4) : charT4 k (x + y) = charT4 k x * charT4 k y

Spatial addition law for a fixed torus character.

noncomputable def Anderson4D.greenPhysicalConvolution (f : C(T4, ℂ)) : C(T4, ℂ)

Convolution by the physical Green kernel on a continuous input. The integral uses the paper's unnormalized torus measure.

Equations

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

theorem Anderson4D.greenPhysicalConvolution_apply (f : C(T4, ℂ)) (x : T4) : (greenPhysicalConvolution f) x = ∫ (y : T4), ↑(greenFn (x - y)) * f y ∂paperMeasure

Symmetric integral form of physical Green convolution.

theorem Anderson4D.paperFourierCoeff_greenPhysicalConvolution (f : C(T4, ℂ)) (k : Z4) : paperFourierCoeff (⇑(greenPhysicalConvolution f)) k = paperFourierCoeff (fun (z : T4) => ↑(greenFn z)) k * paperFourierCoeff (⇑f) k

Fourier transform turns physical Green convolution into multiplication. This version keeps the paper's positive-frequency, unnormalized convention.

theorem Anderson4D.paperFourierCoeff_greenFn_complex_eq_greenL2Symbol (k : Z4) : paperFourierCoeff (fun (z : T4) => ↑(greenFn z)) k = greenL2Symbol k

theorem Anderson4D.torusFourierCoeff_greenPhysicalConvolution (f : C(T4, ℂ)) (k : Z4) : torusFourierCoeff (⇑(greenPhysicalConvolution f)) k = greenL2Symbol k * torusFourierCoeff (⇑f) k

Probability-Haar Fourier coefficient of physical Green convolution. The two measure normalizations cancel exactly.

theorem Anderson4D.greenL2Op_continuousMap (f : C(T4, ℂ)) : greenL2Op ((ContinuousMap.toLp 2 haarT4 ℂ) f) = (ContinuousMap.toLp 2 haarT4 ℂ) (greenPhysicalConvolution f)

The spectral bounded operator and the physical Green convolution agree on every continuous input.

theorem Anderson4D.greenL2Op_continuousMap_action (f : C(T4, ℂ)) : ↑↑(greenL2Op ((ContinuousMap.toLp 2 haarT4 ℂ) f)) =ᵐ[haarT4] fun (x : T4) => ∫ (y : T4), ↑(greenFn (x - y)) * f y ∂paperMeasure

Almost-everywhere pointwise form of the preceding operator identity.