Exact integrated expansion of residual-refined Fourier groups #
The preceding module constructs the pointwise common-increment groups
and proves their joint integrability. Here the summable physical L¹
ledger licenses the exact exchange of the five-group physical integral
with each increment fibre. No decay estimate or target budget enters
this module.
noncomputable def
Anderson4D.SmoothCutoff.r324RefinedRawFourierIntegral
(ρ : SmoothCutoff)
{m : ℕ}
(hm : 0 < m)
(ε : ℝ)
(α β : Z4)
(p : R324RefinedScheduleIndex m)
(a : ℕ)
:
Product-space integral of one raw refined Fourier configuration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.SmoothCutoff.summable_r324RefinedRawFourierIntegral
(ρ : SmoothCutoff)
{m : ℕ}
(hm : 0 < m)
{ε : ℝ}
(hε : 0 < ε)
(α β : Z4)
(p : R324RefinedScheduleIndex m)
:
Summable (ρ.r324RefinedRawFourierIntegral hm ε α β p)
The raw refined Fourier integrals are summable.
theorem
Anderson4D.SmoothCutoff.integral_keyGroupedRefinedEndpointIntegrand_eq_tsumByKey
(ρ : SmoothCutoff)
{m : ℕ}
(hm : 0 < m)
{ε : ℝ}
(hε : 0 < ε)
(α β : Z4)
(p : R324RefinedScheduleIndex m)
(b : ℕ)
:
∫ (q : R324PhysicalPoint m), r324Flatten (ρ.r324KeyGroupedRefinedEndpointIntegrand hm ε α β p b) q ∂r324PhysicalMeasure m = tsumByKey (ρ.r324RefinedRawFourierIntegral hm ε α β p) (r324RefinedRawIncrementKey hm p)
((r324NatEquivStandardConfigurations hm) b)
Exact Fubini exchange for one common-increment group on the genuine five-group product measure.
theorem
Anderson4D.SmoothCutoff.r324GroupedEndpointConfigurationTerm_keyGrouped_eq_tsumByKey
(ρ : SmoothCutoff)
(lam : ℝ)
{m : ℕ}
(hm : 0 < m)
{ε : ℝ}
(hε : 0 < ε)
(α β : Z4)
(p : R324RefinedScheduleIndex m)
(b : ℕ)
:
r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p)
(ρ.r324KeyGroupedRefinedEndpointCore hm ε p b) = ↑(lamEps lam ε) ^ (2 * m) * tsumByKey (ρ.r324RefinedRawFourierIntegral hm ε α β p) (r324RefinedRawIncrementKey hm p)
((r324NatEquivStandardConfigurations hm) b)
A concrete grouped endpoint configuration term is the common coupling factor times the exact raw-integral sum over its shared increment fibre.