Literal DE x DD endpoint factorization and majorant #
This file specializes the parameter carried by the exact DE x DD
collapse to the residual primitive cross factor from paper Step 3. The
remaining endpoint density then factors exactly into one completed DE
half and one completed DD half. The factorization is performed before
any norm is taken.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddCrossCoefficient
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(leftPost : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4)
(rightPost : rightDD.transport.final.SurvivingCoordinate → T4)
:
The untouched Step-3 primitive cross factor on the two completed terminal carriers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddReducedCoefficient
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(outgoingMode : Z4)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(u : (leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) × T4)
(rightPost : rightDD.transport.final.SurvivingCoordinate → T4)
:
Literal parameter supplied to the right DD collapse: the already
completed signed left DE density, the direct right incoming Fourier
scalar, and the still-grouped Step-3 cross factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddFinalRawEndpointDensity_eq_endpointFactors
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(hactive : rightDD.transport.final.state.active.Nonempty)
(leftPost : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4)
(firstLeft : T4)
(rightPost : rightDD.transport.final.SurvivingCoordinate → T4)
:
leftDE.deddFinalRawEndpointDensity rightDD (leftDE.deddReducedCoefficient rightDD beta pi) hactive (-alpha) (-beta)
(leftPost, firstLeft) rightPost = leftDE.outgoing.outgoingEndpointDefectDensity
(leftDE.directIncomingEndpointCoefficient fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1)
alpha beta 0 leftPost firstLeft * rightDD.transportEndpointDensity hactive (leftDE.deddCrossCoefficient rightDD pi leftPost) (-beta) rightPost
Exact product factorization after the left outgoing exceptional operation and both right direct endpoint operations.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddPaperNestedEndpointDensity
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(outgoingMode : Z4)
(hactive : rightDD.transport.final.state.active.Nonempty)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(v : (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD).NestedCoordinate pi → T4)
:
The specialized nested density produced by the exact DE x DD
collapse.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddPaperNestedEndpointDensity_eq_endpointDensity_mul
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(hactive : rightDD.transport.final.state.active.Nonempty)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(v : (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD).NestedCoordinate pi → T4)
:
let terminal := R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD;
have p := (terminal.terminalProductPiMeasurableEquivNested pi).symm v;
leftDE.deddPaperNestedEndpointDensity rightDD beta hactive pi v = leftDE.endpointDensity (fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1) beta 0 p.1 * rightDD.transportEndpointDensity hactive (leftDE.deddCrossCoefficient rightDD pi p.1) (-beta) p.2
Exact Fubini factorization on the common nested carrier. This is the last algebraic step before the first norm in the mixed endpoint branch.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddMassOneGroupedMajorant
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(hright : rightDD.transport.final.state.active.Nonempty)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(leftPost : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4)
(rightPost : rightDD.transport.final.SurvivingCoordinate → T4)
:
The exact positive carrier produced by the mixed DE x DD branch.
There is one inverse-square mass, from the retained exceptional outgoing
endpoint; all three direct Fourier operations are exact multipliers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddEndpointMassCompensation :
Fixed paper constant compensating the three artificial endpoint masses present in the common uniform grouped carrier but absent from the literal mixed calculation.
Equations
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddEndpointCompleteAbsorbedBase
(A C K B : ℝ)
:
Final complete-run base for the mixed branch. Multiplying a fixed positive base once absorbs the order-independent endpoint-mass constant at every positive perturbative order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddEndpointMassCompensation_mul_primitiveInsertedMajorant_le
(B lam eps supportConstant : ℝ)
{n : ℕ}
(hn : 1 ≤ n)
(z : T4)
:
deddEndpointMassCompensation * primitiveInsertedMajorant B lam eps supportConstant n z ≤ primitiveInsertedMajorant (deddEndpointMassCompensation * B) lam eps supportConstant n z
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.deddEndpointMassCompensation_mul_integral_completeAbsorbed_le
(A C K B lam : ℝ)
{eps : ℝ}
(heps : 0 < eps)
(supportConstant : ℝ)
{m : ℕ}
(hm : 1 ≤ m)
:
deddEndpointMassCompensation * ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure ≤ ∫ (z : T4), primitiveInsertedMajorant (deddEndpointCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.norm_endpointDensity_mul_transportEndpointDensity_le_massOneGrouped
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM)
(hright : rightDD.transport.final.state.active.Nonempty)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(leftPost : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4)
(rightPost : rightDD.transport.final.SurvivingCoordinate → T4)
(hneLeft :
∀ edge ∈ leftDE.outgoing.terminalPost.endpointErasedActiveEdgeSlots ⋯,
leftDE.outgoing.terminalPost.edgeDisplacement 0 0 (leftDE.outgoing.terminalPost.reconstruct leftPost) edge ≠ 0)
(hneRight :
∀ edge ∈ rightDD.transport.final.endpointErasedActiveEdgeSlots hright,
rightDD.transport.final.edgeDisplacement 0 0 (rightDD.transport.final.reconstruct rightPost) edge ≠ 0)
:
‖leftDE.endpointDensity (fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1) beta 0 leftPost * rightDD.transportEndpointDensity hright (leftDE.deddCrossCoefficient rightDD pi leftPost) (-beta) rightPost‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps
![SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.insertedSacrifice, SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.directFourier] * leftDE.deddMassOneGroupedMajorant rightDD hright pi leftPost rightPost
Literal pointwise DE x DD estimate before replacing its one real
endpoint mass by the common four-mass grouped currency.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.norm_endpointDensity_mul_transportEndpointDensity_le_compensatedGrouped
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM)
(hright : rightDD.transport.final.state.active.Nonempty)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(leftPost : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4)
(rightPost : rightDD.transport.final.SurvivingCoordinate → T4)
(hneLeft :
∀ edge ∈ leftDE.outgoing.terminalPost.endpointErasedActiveEdgeSlots ⋯,
leftDE.outgoing.terminalPost.edgeDisplacement 0 0 (leftDE.outgoing.terminalPost.reconstruct leftPost) edge ≠ 0)
(hneRight :
∀ edge ∈ rightDD.transport.final.endpointErasedActiveEdgeSlots hright,
rightDD.transport.final.edgeDisplacement 0 0 (rightDD.transport.final.reconstruct rightPost) edge ≠ 0)
:
‖leftDE.endpointDensity (fun (x : leftDE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1) beta 0 leftPost * rightDD.transportEndpointDensity hright (leftDE.deddCrossCoefficient rightDD pi leftPost) (-beta) rightPost‖ ≤ deddEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps
![SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.insertedSacrifice, SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.directFourier]) * (R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE
rightDD).endpointIntegratedGroupedMajorant
leftDE.route.terminalScale rightDD.route.terminalScale ⋯ hright pi (leftPost, rightPost)
The same mixed endpoint estimate in the common grouped Step-3 currency. The sole enlargement is the fixed mass compensation.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.ae_norm_deddPaperNestedEndpointDensity_le_compensatedGrouped
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
(hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM)
(hright : rightDD.transport.final.state.active.Nonempty)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
:
let terminal := R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData leftDE rightDD;
(fun (v : terminal.NestedCoordinate pi → T4) =>
‖leftDE.deddPaperNestedEndpointDensity rightDD beta hright pi
v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) =>
deddEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps
![SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.insertedSacrifice, SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.directFourier]) * terminal.initialNestedEndpointIntegratedGroupedMajorant leftDE.route.terminalScale rightDD.route.terminalScale ⋯
hright pi v
Product-Haar and initial-nested form of the completed mixed endpoint estimate.