Integrability of the completed left endpoint targets #
These are the Fubini licenses used to hand the completed, still signed, left endpoint half to the right endpoint half in paper Step 4(A). They are derived from the same joint integrability statements used by the four exact left transforms. No endpoint norm or majorant is introduced here.
Direct outgoing endpoint #
theorem
Anderson4D.R324WithinHalfResidualPrefix.integrable_leftDirectDirect_targetDensity
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{providers : R324PaperHalfRouteProviders kappaP alpha}
(houtgoing : Fin.last m ∉ extractedRightEdges kappaP)
(data : R324PaperHalfDirectDirectRoute providers)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
:
MeasureTheory.Integrable
(fun (q : R324PaperLeftOuterParameter rho lam eps kappaM × (data.transport.final.SurvivingCoordinate → T4)) =>
(R324PaperHalfEndpointUniformBound.ofDirectDirect houtgoing data).density
(fun (v : (R324PaperHalfEndpointUniformBound.ofDirectDirect houtgoing data).carrier.SurvivingCoordinate → T4) =>
data.transport.final.r324PaperLeftCanonicalCoefficient alpha beta pi q.1 v)
beta q.2)
((r324PaperLeftOuterParameterMeasure rho lam eps kappaM).prod
(MeasureTheory.Measure.pi fun (x : data.transport.final.SurvivingCoordinate) => paperMeasure))
The literal completed DD left density is jointly integrable in the
untouched right-root parameter and the completed left carrier. This is the
terminal certificate L1 statement followed by the exact direct-outgoing
Fourier marginal.
theorem
Anderson4D.R324WithinHalfResidualPrefix.integrable_leftExceptionalDirect_targetDensity
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha beta : Z4}
{providers : R324PaperHalfRouteProviders kappaP alpha}
(houtgoing : Fin.last m ∉ extractedRightEdges kappaP)
(data : R324PaperHalfExceptionalDirectRoute providers)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
:
MeasureTheory.Integrable
(fun (q : R324PaperLeftOuterParameter rho lam eps kappaM × (data.transport.final.SurvivingCoordinate → T4)) =>
(R324PaperHalfEndpointUniformBound.ofExceptionalDirect houtgoing data).density
(fun
(v :
(R324PaperHalfEndpointUniformBound.ofExceptionalDirect houtgoing data).carrier.SurvivingCoordinate → T4) =>
data.transport.final.r324PaperLeftCanonicalCoefficient alpha beta pi q.1 v)
beta q.2)
((r324PaperLeftOuterParameterMeasure rho lam eps kappaM).prod
(MeasureTheory.Measure.pi fun (x : data.transport.final.SurvivingCoordinate) => paperMeasure))
The literal completed ED left density is jointly integrable. The
incoming exceptional head is first collapsed on its signed driver carrier;
the existing direct-outgoing marginal then gives exactly the common target
density.