The right direct-incoming source after the completed left half #
This is the single Fubini/Fourier move used at the interface between the two endpoint halves in paper Step 4(A). The completed left carrier is kept as an untouched parameter, the four factors remain signed, and only then is the right incoming endpoint integrated by the exact initial Green Fourier identity.
No endpoint estimate and no absolute value occurs in this file.
Literal coefficient linearity of the four canonical left routes #
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.density_mul_ofDirectDirect
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(houtgoing : Fin.last m ∉ extractedRightEdges pairing)
(data : R324PaperHalfDirectDirectRoute providers)
(a : ℂ)
(coefficient : (data.transport.final.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(v : data.transport.final.SurvivingCoordinate → T4)
:
(ofDirectDirect houtgoing data).density
(fun (u : (ofDirectDirect houtgoing data).carrier.SurvivingCoordinate → T4) => a * coefficient u) outgoingMode v = a * (ofDirectDirect houtgoing data).density coefficient outgoingMode v
Coefficient linearity for the literal DD density.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.density_mul_ofDirectExceptional
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(a : ℂ)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
:
(ofDirectExceptional data).density
(fun (u : (ofDirectExceptional data).carrier.SurvivingCoordinate → T4) => a * coefficient u) outgoingMode v = a * (ofDirectExceptional data).density coefficient outgoingMode v
Coefficient linearity for the literal DE density.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.density_mul_ofExceptionalDirect
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(houtgoing : Fin.last m ∉ extractedRightEdges pairing)
(data : R324PaperHalfExceptionalDirectRoute providers)
(a : ℂ)
(coefficient : (data.transport.final.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(v : data.transport.final.SurvivingCoordinate → T4)
:
(ofExceptionalDirect houtgoing data).density
(fun (u : (ofExceptionalDirect houtgoing data).carrier.SurvivingCoordinate → T4) => a * coefficient u) outgoingMode
v = a * (ofExceptionalDirect houtgoing data).density coefficient outgoingMode v
Coefficient linearity for the literal ED density.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.density_mul_ofExceptionalExceptional
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(hsingles : pairing.singles.Nonempty)
(data : R324PaperHalfExceptionalExceptionalRoute providers)
(a : ℂ)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
:
(ofExceptionalExceptional hsingles data).density
(fun (u : (ofExceptionalExceptional hsingles data).carrier.SurvivingCoordinate → T4) => a * coefficient u)
outgoingMode v = a * (ofExceptionalExceptional hsingles data).density coefficient outgoingMode v
Coefficient linearity for the literal EE density.
Cross-factor projection for a direct right incoming route #
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324ResidualPrimitiveSumProduct_eq_rightDirectTransportProjection
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{rightMode : Z4}
{rightProviders : R324PaperHalfRouteProviders kappaM rightMode}
(left : R324WithinHalfResidualPrefix rho lam eps kappaP)
(data : R324PaperHalfDirectDirectRoute rightProviders)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(vl : left.SurvivingCoordinate → T4)
(vr : (initial rho lam eps kappaM).SurvivingCoordinate → T4)
:
r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct left (initial rho lam eps kappaM) (vl, vr)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct left data.transport.final (vl, data.transport.projection vr))
A direct right half transported through the full alternating schedule does not change the cross primitive factor.
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324ResidualPrimitiveSumProduct_eq_rightDirectOutgoingTerminalPost
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{rightMode : Z4}
{rightProviders : R324PaperHalfRouteProviders kappaM rightMode}
(left : R324WithinHalfResidualPrefix rho lam eps kappaP)
(data : R324PaperHalfDirectExceptionalRoute rightProviders)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(vl : left.SurvivingCoordinate → T4)
(vr : (initial rho lam eps kappaM).SurvivingCoordinate → T4)
:
r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct left (initial rho lam eps kappaM) (vl, vr)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct left data.outgoing.terminalPost
(vl, ((data.outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv data.outgoing.terminalData.terminal [] ⋯)
(data.outgoing.endpoint.projection vr)).2))
The direct right half with a retained outgoing terminal likewise reads the cross factor on its post-terminal carrier.
The paper's right-incoming regroup #
def
Anderson4D.R324WithinHalfResidualPrefix.r324RightDirectIncomingFourierRegroupMeasurableEquiv
(Z : Type u_1)
(W : Type u_2)
(R : Type u_3)
(L : Type u_4)
[MeasurableSpace Z]
[MeasurableSpace W]
[MeasurableSpace R]
[MeasurableSpace L]
:
Reorder (((z,w),vR),vL) as (((w,vL),vR),z). Thus the incoming
right endpoint z is the last variable, while (w,vL,vR) is exactly the
parameter carrier of the right initial phased density.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324RightDirectIncomingFourierRegroupMeasurableEquiv_apply
{Z : Type u_1}
{W : Type u_2}
{R : Type u_3}
{L : Type u_4}
[MeasurableSpace Z]
[MeasurableSpace W]
[MeasurableSpace R]
[MeasurableSpace L]
(q : ((Z × W) × R) × L)
:
@[simp]
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324RightDirectIncomingFourierRegroupMeasurableEquiv_symm_apply
{Z : Type u_1}
{W : Type u_2}
{R : Type u_3}
{L : Type u_4}
[MeasurableSpace Z]
[MeasurableSpace W]
[MeasurableSpace R]
[MeasurableSpace L]
(q : ((W × L) × R) × Z)
:
theorem
Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324RightDirectIncomingFourierRegroupMeasurableEquiv
{Z : Type u_1}
{W : Type u_2}
{R : Type u_3}
{L : Type u_4}
[MeasurableSpace Z]
[MeasurableSpace W]
[MeasurableSpace R]
[MeasurableSpace L]
(muZ : MeasureTheory.Measure Z)
(muW : MeasureTheory.Measure W)
(muR : MeasureTheory.Measure R)
(muL : MeasureTheory.Measure L)
[MeasureTheory.SFinite muZ]
[MeasureTheory.SFinite muW]
[MeasureTheory.SFinite muR]
[MeasureTheory.SFinite muL]
:
MeasureTheory.MeasurePreserving (⇑(r324RightDirectIncomingFourierRegroupMeasurableEquiv Z W R L))
(((muZ.prod muW).prod muR).prod muL) (((muW.prod muL).prod muR).prod muZ)
The regroup preserves the literal four-factor product measure.
Signed parameterized incoming Fourier collapse #
theorem
Anderson4D.R324WithinHalfResidualPrefix.integrable_and_integral_rightDirectIncomingSource
(rho : SmoothCutoff)
(lam eps : ℝ)
{m : ℕ}
(pairing : PartialPairing (Fin m))
{L : Type u_1}
[MeasurableSpace L]
(muL : MeasureTheory.Measure L)
[MeasureTheory.SFinite muL]
(coefficient : T4 → ((initial rho lam eps pairing).SurvivingCoordinate → T4) → L → ℂ)
(incomingMode : Z4)
(hraw :
MeasureTheory.Integrable
(fun (q : ((T4 × T4) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)) × L) =>
charT4 incomingMode q.1.1.1 * (↑((initial rho lam eps pairing).residualIntegrand rho eps q.1.1.1 q.1.1.2
((initial rho lam eps pairing).reconstruct q.1.2)) * coefficient q.1.1.2 q.1.2 q.2))
(((paperMeasure.prod paperMeasure).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure)).prod
muL))
:
MeasureTheory.Integrable
(fun (q : (T4 × L) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)) =>
(initial rho lam eps pairing).incomingPhasedResidualDensity
(↑(paperSecondOrderModeDecay incomingMode) * coefficient q.1.1 q.2 q.1.2) incomingMode rho eps 0 q.1.1 q.2)
((paperMeasure.prod muL).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure)) ∧ ∫ (s : (T4 × T4) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)), ∫ (u : L), charT4 incomingMode s.1.1 * (↑((initial rho lam eps pairing).residualIntegrand rho eps s.1.1 s.1.2
((initial rho lam eps pairing).reconstruct s.2)) * coefficient s.1.2 s.2
u) ∂muL ∂(paperMeasure.prod paperMeasure).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure) = ∫ (q : (T4 × L) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)), (initial rho lam eps pairing).incomingPhasedResidualDensity
(↑(paperSecondOrderModeDecay incomingMode) * coefficient q.1.1 q.2 q.1.2) incomingMode rho eps 0 q.1.1
q.2 ∂(paperMeasure.prod muL).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure)
The completed left carrier may occur in an arbitrary signed scalar
coefficient. Joint integrability of the genuine pre-Fourier density is
the only Fubini premise. The conclusion supplies both the integrability
of the right initial source and its exact equality with the regrouped left
integral.
The four canonical left endpoint densities are plugged into coefficient
by small pointwise adapters; this theorem deliberately does not assume a
new abstract linearity field on the common endpoint interface.
Branch-specific source equalities are assembled at their call sites from the generic theorem above and the four strict-green density-linearity lemmas. Keeping a second wrapper here only duplicated elaboration.