Coefficient-parametric two-half endpoint exit #
Paper Step 4 applies all four signed endpoint operations while the complete signed-word coefficient is still untouched. This file records that fact at the common two-half carrier: the coefficient may be any function of the two surviving half configurations. In particular, no block-local factorization of the coefficient is assumed.
The resulting estimate retains, as global factors, both fourth-order mode decays and the four-route endpoint sacrifice. The remaining spatial majorant contains exactly the two terminal scale products, the two endpoint-erased inverse-square paths, and the norm of the original complete coefficient.
def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.endpointProductDensityWithCoefficient
{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)
(beta : Z4)
(coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ)
(p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4))
:
The ordered four-endpoint density with an arbitrary complete coefficient. The right endpoint transform is applied only after the completed left density has been formed, so the coefficient is never split between grouped blocks.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.nestedEndpointProductDensityWithCoefficient
{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)
(beta : Z4)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ)
(v : (left.twoHalfTerminal right).NestedCoordinate pi → T4)
:
The coefficient-parametric density on the literal initial nested-cross carrier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.coefficientEndpointGroupedMajorant
{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)
(coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ)
(p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4))
:
The spatial part of the coefficient-parametric endpoint majorant. The mode decay and endpoint sacrifice deliberately do not occur here: they stay outside the complete signed-word coefficient and outside every grouped run.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.initialNestedCoefficientEndpointGroupedMajorant
{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)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ)
(v : (left.twoHalfTerminal right).NestedCoordinate pi → T4)
:
The preceding spatial majorant transported to the initial nested-cross carrier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.norm_endpointProductDensityWithCoefficient_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)}
(routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders)
(left : R324PaperHalfEndpointUniformBound routes.left.completedRoute)
(right : R324PaperHalfEndpointUniformBound routes.right.completedRoute)
(coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ)
(p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4))
(hneLeft :
∀ edge ∈ left.carrier.endpointErasedActiveEdgeSlots ⋯,
left.carrier.edgeDisplacement 0 0 (left.carrier.reconstruct p.1) edge ≠ 0)
(hneRight :
∀ edge ∈ right.carrier.endpointErasedActiveEdgeSlots ⋯,
right.carrier.edgeDisplacement 0 0 (right.carrier.reconstruct p.2) edge ≠ 0)
:
‖left.endpointProductDensityWithCoefficient right beta coefficient p‖ ≤ twoHalfEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases) * left.coefficientEndpointGroupedMajorant right coefficient p
Pointwise paper Step 4(A) estimate for an arbitrary complete two-half coefficient. The four signed endpoint operations occur before this theorem takes a norm.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ae_norm_nestedEndpointProductDensityWithCoefficient_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)}
(routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders)
(left : R324PaperHalfEndpointUniformBound routes.left.completedRoute)
(right : R324PaperHalfEndpointUniformBound routes.right.completedRoute)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ)
:
(fun (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4) =>
‖left.nestedEndpointProductDensityWithCoefficient right beta pi coefficient
v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure] fun (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4) =>
twoHalfEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases) * left.initialNestedCoefficientEndpointGroupedMajorant right pi coefficient v
The coefficient-parametric endpoint exit on the initial nested carrier.
@[simp]
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.endpointProductDensityWithCoefficient_crossCoefficient
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders)
(left : R324PaperHalfEndpointUniformBound routes.left.completedRoute)
(right : R324PaperHalfEndpointUniformBound routes.right.completedRoute)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4))
:
left.endpointProductDensityWithCoefficient right beta (left.crossCoefficient right pi) p = left.endpointProductDensity right beta pi p
The former residual-primitive endpoint density is the exact specialization of the coefficient-parametric construction.
@[simp]
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.nestedEndpointProductDensityWithCoefficient_crossCoefficient
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP alpha}
{rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)}
(routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders)
(left : R324PaperHalfEndpointUniformBound routes.left.completedRoute)
(right : R324PaperHalfEndpointUniformBound routes.right.completedRoute)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(v : (left.twoHalfTerminal right).NestedCoordinate pi → T4)
:
left.nestedEndpointProductDensityWithCoefficient right beta pi (left.crossCoefficient right pi) v = left.nestedEndpointProductDensity right beta pi v
The preceding specialization is also definitional after transport to the initial nested carrier.