Common ordered carrier after the four paper endpoint operations

The branch-specific signed transforms stop at one common object: first the left completed density is formed with the still-grouped residual primitive factor as its coefficient, then that signed scalar is left untouched while the right completed density is formed. This is the literal order of the two applications in paper Step 4(A), so no coefficient-linearity lemma or premature Fubini step is needed. This file names that object and transports it to the initial nested-cross carrier. It performs no estimate.

def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.twoHalfTerminal {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftRoute : R324PaperHalfCompletedRoute kappaP alpha} {rightRoute : R324PaperHalfCompletedRoute kappaM (-alpha)} (left : R324PaperHalfEndpointUniformBound leftRoute) (right : R324PaperHalfEndpointUniformBound rightRoute) : R324TwoHalfTerminalData rho lam eps kappaP kappaM

The terminal built from the two literal carriers retained by the uniform one-half packages.

Equations

• left.twoHalfTerminal right = { left := left.carrier, right := right.carrier, left_remaining := ⋯, right_remaining := ⋯, left_processed := ⋯, right_processed := ⋯ }

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.crossCoefficient {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftRoute : R324PaperHalfCompletedRoute kappaP alpha} {rightRoute : R324PaperHalfCompletedRoute kappaM (-alpha)} (left : R324PaperHalfEndpointUniformBound leftRoute) (right : R324PaperHalfEndpointUniformBound rightRoute) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (leftPost : left.carrier.SurvivingCoordinate → T4) (rightPost : right.carrier.SurvivingCoordinate → T4) : ℂ

The untouched Step-3 primitive cross factor on the two completed endpoint carriers.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.endpointProductDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftRoute : R324PaperHalfCompletedRoute kappaP alpha} {rightRoute : R324PaperHalfCompletedRoute kappaM (-alpha)} (left : R324PaperHalfEndpointUniformBound leftRoute) (right : R324PaperHalfEndpointUniformBound rightRoute) (beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) : ℂ

Literal ordered density after both endpoints of both halves have been evaluated. The residual primitive factor first enters as the left coefficient; the completed left signed density is then the untouched coefficient of the right endpoint operation. This is definitionally the target of ExactTransform.compose.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.nestedEndpointProductDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftRoute : R324PaperHalfCompletedRoute kappaP alpha} {rightRoute : R324PaperHalfCompletedRoute kappaM (-alpha)} (left : R324PaperHalfEndpointUniformBound leftRoute) (right : R324PaperHalfEndpointUniformBound rightRoute) (beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4) : ℂ

The same signed density on the literal initial nested-cross carrier.

Equations

• left.nestedEndpointProductDensity right beta pi v = (left.twoHalfTerminal right).initialNestedPullback pi (left.endpointProductDensity right beta pi) v

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.integral_endpointProductDensity_eq_nested {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftRoute : R324PaperHalfCompletedRoute kappaP alpha} {rightRoute : R324PaperHalfCompletedRoute kappaM (-alpha)} (left : R324PaperHalfEndpointUniformBound leftRoute) (right : R324PaperHalfEndpointUniformBound rightRoute) (beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) : ∫ (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)), left.endpointProductDensity right beta pi p ∂(MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure) = ∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), left.nestedEndpointProductDensity right beta pi v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure

Product Haar and initial nested Haar give exactly the same signed four-endpoint integral.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.twoHalfTerminal_eq_routes {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP alpha} {rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) (left : R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324PaperHalfEndpointUniformBound routes.right.completedRoute) : left.twoHalfTerminal right = routes.terminal

The terminal retained by the uniform packages is canonically the same terminal retained by their structural routes.