Exact two-half composition at the common paper endpoint carrier #
This file contains the single algebraic/Fubini seam shared by all actual
endpoint cases. The branch-specific work stops when it supplies the two
already proved one-half ExactTransforms and identifies the second source
with the first target. The two transforms are then composed before any
norm is taken, and the completed signed density is transported once to the
initial nested-cross carrier.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.exactCollapse_to_nested_of_transforms
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftRoute : R324PaperHalfCompletedRoute kappaP alpha}
{rightRoute : R324PaperHalfCompletedRoute kappaM (-alpha)}
(left : R324PaperHalfEndpointUniformBound leftRoute)
(right : R324PaperHalfEndpointUniformBound rightRoute)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
(leftCoefficient : U → (left.carrier.SurvivingCoordinate → T4) → ℂ)
(leftTransform : left.ExactTransform muU leftCoefficient beta)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(rightTransform :
right.ExactTransform (MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure)
(fun (leftPost : left.carrier.SurvivingCoordinate → T4) (rightPost : right.carrier.SurvivingCoordinate → T4) =>
left.density
(fun (x : left.carrier.SurvivingCoordinate → T4) => left.crossCoefficient right pi leftPost rightPost) beta
leftPost)
(-beta))
(hsource : rightTransform.source = left.transformTarget muU leftCoefficient beta)
(physical : ℂ)
(hphysical : leftTransform.source = physical)
(hintegrable :
MeasureTheory.Integrable (left.endpointProductDensity right beta pi)
((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod
(MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))
:
↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), left.nestedEndpointProductDensity right beta pi
v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure
The common consumer of the two branch-literal one-half transforms.
The right coefficient is exactly the completed left signed density with the
untouched primitive cross factor. Consequently its target is
definitionally endpointProductDensity; the only Fubini step is the final
product-Haar regroup, justified by the displayed integrability premise.