Exact signed DE x DD composition for paper Step 4(A)

The left retained terminal has already been evaluated by the ordinary-J identity. Its completed carrier and free endpoint are then kept as one untouched parameter while the right direct/direct half is transported and Fourier-integrated. No norm or pointwise majorant occurs in this file.

The one-free-endpoint Fubini regroup

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324DEDDEndpointRegroupMeasurableEquiv (L : Type u_1) (R : Type u_2) [MeasurableSpace L] [MeasurableSpace R] : (L × T4) × R ≃ᵐ (L × R) × T4

Regroup ((left, firstLeft), right) as ((left, right), firstLeft).

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324DEDDEndpointRegroupMeasurableEquiv_apply {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (q : (L × T4) × R) : (r324DEDDEndpointRegroupMeasurableEquiv L R) q = ((q.1.1, q.2), q.1.2)

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324DEDDEndpointRegroupMeasurableEquiv_symm_apply {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (q : (L × R) × T4) : (r324DEDDEndpointRegroupMeasurableEquiv L R).symm q = ((q.1.1, q.2), q.1.2)

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324DEDDEndpointRegroupMeasurableEquiv {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (muL : MeasureTheory.Measure L) (muR : MeasureTheory.Measure R) [MeasureTheory.SFinite muL] [MeasureTheory.SFinite muR] : MeasureTheory.MeasurePreserving (⇑(r324DEDDEndpointRegroupMeasurableEquiv L R)) ((muL.prod paperMeasure).prod muR) ((muL.prod muR).prod paperMeasure)

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_deddEndpoint_regroup {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (muL : MeasureTheory.Measure L) (muR : MeasureTheory.Measure R) [MeasureTheory.SFinite muL] [MeasureTheory.SFinite muR] (F : (L × T4) × R → ℂ) (hF : MeasureTheory.Integrable F ((muL.prod paperMeasure).prod muR)) : ∫ (u : L × T4), ∫ (v : R), F (u, v) ∂muR ∂muL.prod paperMeasure = ∫ (p : L × R), ∫ (firstLeft : T4), F ((p.1, firstLeft), p.2) ∂paperMeasure ∂muL.prod muR

Fubini is used only on the jointly integrable density after the left ordinary-J operation and the right direct Fourier operation are both complete.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddFinalRawEndpointDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (leftDE : R324PaperHalfDirectExceptionalRoute leftProviders) (rightDD : R324PaperHalfDirectDirectRoute rightProviders) (red : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4 → (rightDD.transport.final.SurvivingCoordinate → T4) → ℂ) (hactive : rightDD.transport.final.state.active.Nonempty) (rightIncomingMode rightOutgoingMode : Z4) (u : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4) (v : rightDD.transport.final.SurvivingCoordinate → T4) : ℂ

The literal signed density after the left DE operation and the right DD operation have both finished. The left free endpoint is part of the parameter u; the right direct outgoing endpoint has already been Fourier integrated.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.lamEps_pow_twoHalfPhysical_eq_deddFinalRaw_of_rightDirect {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (leftDE : R324PaperHalfDirectExceptionalRoute leftProviders) (rightDD : R324PaperHalfDirectDirectRoute rightProviders) (physical : ℂ) (red : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4 → (rightDD.transport.final.SurvivingCoordinate → T4) → ℂ) (rightIncomingMode rightOutgoingMode : Z4) (hleftCollapse : ↑(lamEps lam eps) ^ (2 * (initial rho lam eps kappaP).remainingOrder) * physical = ∫ (q : (T4 × (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)), (initial rho lam eps kappaM).incomingPhasedResidualDensity (charT4 rightOutgoingMode q.1.1 * red q.1.2 (rightDD.transport.projection q.2)) rightIncomingMode rho eps 0 q.1.1 q.2 ∂(paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)) (hcurrent : MeasureTheory.Integrable (fun (q : (T4 × (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) => (initial rho lam eps kappaM).incomingPhasedResidualDensity (charT4 rightOutgoingMode q.1.1 * red q.1.2 (rightDD.transport.projection q.2)) rightIncomingMode rho eps 0 q.1.1 q.2) ((paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure))) (hactive : rightDD.transport.final.state.active.Nonempty) (hedge : rightDD.transport.final.state.edges (rightDD.transport.final.terminalOutgoingEdgeSlot hactive) = greenFn) (hterminal : MeasureTheory.Integrable (fun (q : (T4 × (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightDD.transport.final.SurvivingCoordinate → T4)) => rightDD.transport.final.incomingPhasedResidualDensity (charT4 rightOutgoingMode q.1.1 * (rightDD.transport.multiplier rightIncomingMode * red q.1.2 q.2)) rightIncomingMode rho eps 0 q.1.1 q.2) ((paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure)).prod (MeasureTheory.Measure.pi fun (x : rightDD.transport.final.SurvivingCoordinate) => paperMeasure))) : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (u : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4), ∫ (v : rightDD.transport.final.SurvivingCoordinate → T4), leftDE.deddFinalRawEndpointDensity rightDD red hactive rightIncomingMode rightOutgoingMode u v ∂MeasureTheory.Measure.pi fun (x : rightDD.transport.final.SurvivingCoordinate) => paperMeasure ∂(MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure

Algebraic composition of a completed left DE collapse with the parameterized right DD theorem. hleftCollapse is precisely the signed output of the left retained-terminal identity after the harmless product reassociation that places the right initial carrier last.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddNestedEndpointDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (leftDE : R324PaperHalfDirectExceptionalRoute leftProviders) (rightDD : R324PaperHalfDirectDirectRoute rightProviders) (red : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4 → (rightDD.transport.final.SurvivingCoordinate → T4) → ℂ) (hactive : rightDD.transport.final.state.active.Nonempty) (rightIncomingMode rightOutgoingMode : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (v : (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD).NestedCoordinate pi → T4) : ℂ

Reindex the completed DE x DD density onto the literal nested carrier used by the common Step-3/Step-4 numerical exit.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.integral_deddFinalRaw_eq_integral_nestedEndpointDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (leftDE : R324PaperHalfDirectExceptionalRoute leftProviders) (rightDD : R324PaperHalfDirectDirectRoute rightProviders) (red : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4 → (rightDD.transport.final.SurvivingCoordinate → T4) → ℂ) (hactive : rightDD.transport.final.state.active.Nonempty) (rightIncomingMode rightOutgoingMode : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hraw : MeasureTheory.Integrable (fun (q : ((leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightDD.transport.final.SurvivingCoordinate → T4)) => leftDE.deddFinalRawEndpointDensity rightDD red hactive rightIncomingMode rightOutgoingMode q.1 q.2) (((MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : rightDD.transport.final.SurvivingCoordinate) => paperMeasure))) : ∫ (u : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4), ∫ (v : rightDD.transport.final.SurvivingCoordinate → T4), leftDE.deddFinalRawEndpointDensity rightDD red hactive rightIncomingMode rightOutgoingMode u v ∂MeasureTheory.Measure.pi fun (x : rightDD.transport.final.SurvivingCoordinate) => paperMeasure ∂(MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure = ∫ (v : (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD).NestedCoordinate pi → T4), leftDE.deddNestedEndpointDensity rightDD red hactive rightIncomingMode rightOutgoingMode pi v ∂MeasureTheory.Measure.pi fun (x : (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD).NestedCoordinate pi) => paperMeasure

Final Fubini/reindexing after both endpoint operations.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.lamEps_pow_twoHalfPhysical_eq_deddNested_of_raw {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (leftDE : R324PaperHalfDirectExceptionalRoute leftProviders) (rightDD : R324PaperHalfDirectDirectRoute rightProviders) (physical : ℂ) (red : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4 → (rightDD.transport.final.SurvivingCoordinate → T4) → ℂ) (hactive : rightDD.transport.final.state.active.Nonempty) (rightIncomingMode rightOutgoingMode : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hrawCollapse : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (u : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4), ∫ (v : rightDD.transport.final.SurvivingCoordinate → T4), leftDE.deddFinalRawEndpointDensity rightDD red hactive rightIncomingMode rightOutgoingMode u v ∂MeasureTheory.Measure.pi fun (x : rightDD.transport.final.SurvivingCoordinate) => paperMeasure ∂(MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure) (hraw : MeasureTheory.Integrable (fun (q : ((leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightDD.transport.final.SurvivingCoordinate → T4)) => leftDE.deddFinalRawEndpointDensity rightDD red hactive rightIncomingMode rightOutgoingMode q.1 q.2) (((MeasureTheory.Measure.pi fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : rightDD.transport.final.SurvivingCoordinate) => paperMeasure))) : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (v : (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD).NestedCoordinate pi → T4), leftDE.deddNestedEndpointDensity rightDD red hactive rightIncomingMode rightOutgoingMode pi v ∂MeasureTheory.Measure.pi fun (x : (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD).NestedCoordinate pi) => paperMeasure

Consumer form: any exact product-carrier DE x DD collapse is carried without loss to the common nested endpoint density.