Fourier and Gram form of the four-point Green kernel

This file supplies the analytic bridge needed by node D-limit. It first computes the Fourier coefficient of a translated Green kernel, then packages two such coefficients as a mode profile. The final Fubini theorem identifies fourPointHCoeff with the bilinear Gram integral of two profiles.

Measurability and translation of the Green kernel

theorem Anderson4D.measurable_heatKernelT4_prod : Measurable fun (p : ℝ × T4) => heatKernelT4 p.1 p.2

Joint measurability of the heat kernel, exposed here because the corresponding implementation lemma in GreenFourier is private.

theorem Anderson4D.measurable_greenFn : Measurable greenFn

The heat-integral construction of the Green kernel is measurable.

theorem Anderson4D.integrable_greenFn_sub (z : T4) : MeasureTheory.Integrable (fun (x : T4) => greenFn (x - z)) paperMeasure

Translation preserves the L¹ property of the Green kernel.

theorem Anderson4D.integral_greenFn_sub (z : T4) : ∫ (x : T4), greenFn (x - z) ∂paperMeasure = 1

Every translate of the Green kernel has paper mass one.

One-mode coefficients and two-mode profiles

noncomputable def Anderson4D.translatedGreenMode (k : Z4) (z : T4) : ℂ

The positive-exponential Fourier coefficient of the Green kernel translated to the point z.

Equations

• Anderson4D.translatedGreenMode k z = ∫ (x : Anderson4D.T4), Anderson4D.charT4 k x * ↑(Anderson4D.greenFn (x - z)) ∂Anderson4D.paperMeasure

theorem Anderson4D.translatedGreenMode_eq (k : Z4) (z : T4) : translatedGreenMode k z = charT4 k z * ↑(1 + ∑ i : Fin dim, ↑(k i) ^ 2)⁻¹

Explicit translated Fourier coefficient of G.

noncomputable def Anderson4D.fourPointModeProfile (α β : Z4) (z : T4) : ℂ

The two-external-leg mode profile at the common contraction point.

Equations

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

theorem Anderson4D.fourPointModeProfile_eq_mul_translated (α β : Z4) (z : T4) : fourPointModeProfile α β z = translatedGreenMode α z * translatedGreenMode β z

The double integral defining a profile factors into the two translated one-mode coefficients.

theorem Anderson4D.fourPointModeProfile_eq (α β : Z4) (z : T4) : fourPointModeProfile α β z = charT4 α z * ↑(1 + ∑ i : Fin dim, ↑(α i) ^ 2)⁻¹ * (charT4 β z * ↑(1 + ∑ i : Fin dim, ↑(β i) ^ 2)⁻¹)

Explicit Fourier character formula for the mode profile.

Absolute integrability of the five-variable kernel

@[reducible, inline]

abbrev Anderson4D.FourPointExternal : Type

Right-associated carrier for the four external variables (x₁,y₁,x₂,y₂).

Equations

• Anderson4D.FourPointExternal = (Anderson4D.T4 × Anderson4D.T4 × Anderson4D.T4 × Anderson4D.T4)

noncomputable def Anderson4D.fourPointExternalMeasure : MeasureTheory.Measure FourPointExternal

Product paper measure on the four external variables.

Equations

• Anderson4D.fourPointExternalMeasure = Anderson4D.paperMeasure.prod (Anderson4D.paperMeasure.prod (Anderson4D.paperMeasure.prod Anderson4D.paperMeasure))

instance Anderson4D.instSFiniteFourPointExternalFourPointExternalMeasure : MeasureTheory.SFinite fourPointExternalMeasure

instance Anderson4D.instIsFiniteMeasureFourPointExternalFourPointExternalMeasure : MeasureTheory.IsFiniteMeasure fourPointExternalMeasure

noncomputable def Anderson4D.greenModeFactor (k : Z4) (z x : T4) : ℂ

One character-decorated Green leg.

Equations

• Anderson4D.greenModeFactor k z x = Anderson4D.charT4 k x * ↑(Anderson4D.greenFn (x - z))

noncomputable def Anderson4D.fourPointFourierIntegrand (α₁ β₁ α₂ β₂ : Z4) (p : FourPointExternal) (z : T4) : ℂ

The full five-variable Fourier integrand, with the four external variables grouped separately from their common contraction point.

Equations

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

theorem Anderson4D.measurable_greenModeFactor_joint (k : Z4) : Measurable fun (p : T4 × T4) => greenModeFactor k p.2 p.1

theorem Anderson4D.integrable_greenModeFactor (k : Z4) (z : T4) : MeasureTheory.Integrable (greenModeFactor k z) paperMeasure

A character-decorated translated Green leg is integrable.

theorem Anderson4D.integral_norm_greenModeFactor (k : Z4) (z : T4) : ∫ (x : T4), ‖greenModeFactor k z x‖ ∂paperMeasure = 1

The L¹ norm of one decorated leg is exactly one.

theorem Anderson4D.integrable_fourPointFourierIntegrand_section (α₁ β₁ α₂ β₂ : Z4) (z : T4) : MeasureTheory.Integrable (fun (p : FourPointExternal) => fourPointFourierIntegrand α₁ β₁ α₂ β₂ p z) fourPointExternalMeasure

For each fixed contraction point, the product of the four external Green legs is integrable.

theorem Anderson4D.integral_norm_fourPointFourierIntegrand_section (α₁ β₁ α₂ β₂ : Z4) (z : T4) : ∫ (p : FourPointExternal), ‖fourPointFourierIntegrand α₁ β₁ α₂ β₂ p z‖ ∂fourPointExternalMeasure = 1

The integral of the norm of the four-leg section is one.

theorem Anderson4D.measurable_fourPointFourierIntegrand (α₁ β₁ α₂ β₂ : Z4) : Measurable fun (q : FourPointExternal × T4) => fourPointFourierIntegrand α₁ β₁ α₂ β₂ q.1 q.2

Joint measurability of the five-variable Fourier integrand.

theorem Anderson4D.integrable_fourPointFourierIntegrand (α₁ β₁ α₂ β₂ : Z4) : MeasureTheory.Integrable (fun (q : FourPointExternal × T4) => fourPointFourierIntegrand α₁ β₁ α₂ β₂ q.1 q.2) (fourPointExternalMeasure.prod paperMeasure)

The complete five-variable Fourier kernel is absolutely integrable. This global statement is what permits the safe block Fubini swap; some lower-dimensional pointwise sections at coincident external points are not integrable.

Block Fubini and the Gram identity

theorem Anderson4D.integral_fourPointFourierIntegrand_external (α₁ β₁ α₂ β₂ : Z4) (z : T4) : ∫ (p : FourPointExternal), fourPointFourierIntegrand α₁ β₁ α₂ β₂ p z ∂fourPointExternalMeasure = fourPointModeProfile α₁ β₁ z * fourPointModeProfile α₂ β₂ z

Integrating the external variables of the five-variable kernel produces the product of its two mode profiles.

theorem Anderson4D.fourPointHCoeff_eq_profileGram (α₁ β₁ α₂ β₂ : Z4) : fourPointHCoeff α₁ β₁ α₂ β₂ = ∫ (z : T4), fourPointModeProfile α₁ β₁ z * fourPointModeProfile α₂ β₂ z ∂paperMeasure

Gram bridge for D-limit. The four-point Fourier coefficient is the bilinear Gram integral of the two mode profiles.

Hermitian and explicit Fourier forms

noncomputable def Anderson4D.greenModeWeight (k : Z4) : ℝ

The real nonnegative Fourier multiplier of one Green leg.

Equations

• Anderson4D.greenModeWeight k = (1 + ∑ i : Fin Anderson4D.dim, ↑(k i) ^ 2)⁻¹

theorem Anderson4D.greenModeWeight_nonneg (k : Z4) : 0 ≤ greenModeWeight k

@[simp]

theorem Anderson4D.greenModeWeight_neg (k : Z4) : greenModeWeight (-k) = greenModeWeight k

theorem Anderson4D.fourPointModeProfile_eq_character (α β : Z4) (z : T4) : fourPointModeProfile α β z = ↑(greenModeWeight α * greenModeWeight β) * charT4 (α + β) z

Compact character presentation of the two-leg profile.

theorem Anderson4D.fourPointModeProfile_neg (α β : Z4) (z : T4) : fourPointModeProfile (-α) (-β) z = (starRingEnd ℂ) (fourPointModeProfile α β z)

Negating both modes conjugates the profile.

theorem Anderson4D.fourPointHCoeff_neg_eq_profileInner (α₁ β₁ α₂ β₂ : Z4) : fourPointHCoeff α₁ β₁ (-α₂) (-β₂) = ∫ (z : T4), fourPointModeProfile α₁ β₁ z * (starRingEnd ℂ) (fourPointModeProfile α₂ β₂ z) ∂paperMeasure

Hermitian Gram form obtained by negating the modes of the second profile. This is the form directly consumed by covariance PSD proofs.

theorem Anderson4D.integral_charT4_paper (k : Z4) : ∫ (z : T4), charT4 k z ∂paperMeasure = if k = 0 then ↑((2 * Real.pi) ^ dim) else 0

Paper-normalized integral of one product character.

theorem Anderson4D.fourPointHCoeff_eq_indicator (α₁ β₁ α₂ β₂ : Z4) : fourPointHCoeff α₁ β₁ α₂ β₂ = if α₁ + β₁ + (α₂ + β₂) = 0 then ↑((2 * Real.pi) ^ dim) * ↑(greenModeWeight α₁ * greenModeWeight β₁ * greenModeWeight α₂ * greenModeWeight β₂) else 0

Fully explicit four-point Fourier coefficient. Frequency is conserved at the common contraction point, and the remaining factor is the product of the four Green multipliers.

Finite Gram quadratic forms

noncomputable def Anderson4D.fourPointProfileCombination {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (z : T4) : ℂ

Finite linear combination of two-leg mode profiles.

Equations

• Anderson4D.fourPointProfileCombination modes c z = ∑ i : Fin s, c i * Anderson4D.fourPointModeProfile (modes i).1 (modes i).2 z

theorem Anderson4D.continuous_fourPointModeProfile (α β : Z4) : Continuous (fourPointModeProfile α β)

theorem Anderson4D.continuous_fourPointProfileCombination {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Continuous (fourPointProfileCombination modes c)

theorem Anderson4D.integrable_fourPointProfileCombination_mul_conj {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : MeasureTheory.Integrable (fun (z : T4) => fourPointProfileCombination modes c z * (starRingEnd ℂ) (fourPointProfileCombination modes c z)) paperMeasure

theorem Anderson4D.sum_fourPointHCoeff_neg_eq_profileCombination {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ∑ i : Fin s, ∑ j : Fin s, c i * (starRingEnd ℂ) (c j) * fourPointHCoeff (modes i).1 (modes i).2 (-(modes j).1) (-(modes j).2) = ∫ (z : T4), fourPointProfileCombination modes c z * (starRingEnd ℂ) (fourPointProfileCombination modes c z) ∂paperMeasure

Finite Hermitian covariance quadratic form equals the squared L² norm of the corresponding profile combination.

theorem Anderson4D.sum_fourPointHCoeff_neg_re_nonneg {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : 0 ≤ (∑ i : Fin s, ∑ j : Fin s, c i * (starRingEnd ℂ) (c j) * fourPointHCoeff (modes i).1 (modes i).2 (-(modes j).1) (-(modes j).2)).re

The finite Hermitian four-point covariance form is positive semidefinite.