Completed-left handoff to a direct right incoming endpoint #
This is the literal Fubini handoff between the two halves in paper Section 4.2, Step 4(A). The already completed left density stays signed. After its scalar outer factors are pulled through the left density, the right incoming Fourier variable is integrated by the existing exact initial-residual identity. No norm or endpoint estimate occurs here.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.integrable_and_integral_completedLeft_eq_rightDirectInitialSource
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
{leftRoute : R324PaperHalfCompletedRoute kappaP alpha}
(left : R324PaperHalfEndpointUniformBound leftRoute)
(beta : Z4)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
{RightPost : Type u_1}
[MeasurableSpace RightPost]
(project : ((initial rho lam eps kappaM).SurvivingCoordinate → T4) → RightPost)
(projectedCoefficient : (left.carrier.SurvivingCoordinate → T4) → RightPost → ℂ)
(hlinear :
∀ (a : ℂ) (coefficient : (left.carrier.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4)
(v : left.carrier.SurvivingCoordinate → T4),
left.density (fun (u : left.carrier.SurvivingCoordinate → T4) => a * coefficient u) outgoingMode v = a * left.density coefficient outgoingMode v)
(hproject :
∀ (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : left.carrier.SurvivingCoordinate → T4),
↑(r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi
(r324TwoHalfRootDoubledReconstruct left.carrier (initial rho lam eps kappaM) (v, s.2))) = projectedCoefficient v (project s.2))
(hleft :
MeasureTheory.Integrable
(fun (q : R324PaperLeftOuterParameter rho lam eps kappaM × (left.carrier.SurvivingCoordinate → T4)) =>
left.density
(fun (v : left.carrier.SurvivingCoordinate → T4) =>
left.carrier.r324PaperLeftCanonicalCoefficient alpha beta pi q.1 v)
beta q.2)
((r324PaperLeftOuterParameterMeasure rho lam eps kappaM).prod
(MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure)))
:
MeasureTheory.Integrable
(fun
(q :
(T4 × (left.carrier.SurvivingCoordinate → T4)) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) =>
(initial rho lam eps kappaM).incomingPhasedResidualDensity
(↑(paperSecondOrderModeDecay (-alpha)) * (charT4 (-beta) q.1.1 * left.density (fun (v : left.carrier.SurvivingCoordinate → T4) => projectedCoefficient v (project q.2)) beta
q.1.2))
(-alpha) rho eps 0 q.1.1 q.2)
((paperMeasure.prod (MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure)).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)) ∧ left.transformTarget (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)
(fun (s : R324PaperLeftOuterParameter rho lam eps kappaM) (v : left.carrier.SurvivingCoordinate → T4) =>
left.carrier.r324PaperLeftCanonicalCoefficient alpha beta pi s v)
beta = ∫ (q : (T4 × (left.carrier.SurvivingCoordinate → T4)) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)), (initial rho lam eps kappaM).incomingPhasedResidualDensity
(↑(paperSecondOrderModeDecay (-alpha)) * (charT4 (-beta) q.1.1 * left.density (fun (v : left.carrier.SurvivingCoordinate → T4) => projectedCoefficient v (project q.2)) beta
q.1.2))
(-alpha) rho eps 0 q.1.1
q.2 ∂(paperMeasure.prod
(MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure)).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)
Exact direct-incoming handoff for an arbitrary completed left route.
project is the already proved right transport projection (either the
full direct transport or the retained outgoing-terminal projection), and
hproject is precisely the corresponding primitive-cross identity.