Exact exceptional/exceptional one-half transform #
This file is the literal EE instance of the common signed transform
interface. It only packages the parameter-carrier identity already proved
for the incoming exceptional head and retained outgoing terminal.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.ofExceptionalExceptional
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(hsingles : pairing.singles.Nonempty)
(data : R324PaperHalfExceptionalExceptionalRoute providers)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
[MeasureTheory.SFinite muU]
(coefficient : U → (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(hG :
∀ (j : Fin (2 * residualBlockOrder data.pack.data.stopContext.step.2 - 1)),
MemEClassT4 (data.pack.data.stopContext.internalEdges j))
(hincoming :
∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.pack.data.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.pack.data.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.pack.data.terminal.2) (↑kappaB)
data.pack.data.stopContext.internalEdges
(primitiveAssemble (residualBlockOrder data.pack.data.terminal.2) ⋯ first (first + gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.pack.data.terminal.2 - 2)) => paperMeasure))
(hcurrent :
MeasureTheory.Integrable
(data.pack.data.incomingExceptionalInitialSourceDensity incomingMode (fun (omega : T4 × U) => omega.1)
fun (omega : T4 × U)
(v :
(data.pack.data.trace.stopPrefix.afterHead data.pack.data.terminal data.pack.data.suffix
⋯).SurvivingCoordinate →
T4) =>
charT4 outgoingMode omega.1 * coefficient omega.2
((data.outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv data.outgoing.terminalData.terminal [] ⋯)
(data.outgoing.endpoint.projection v)).2)
((paperMeasure.prod (paperMeasure.prod muU)).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure)))
(hsource :
MeasureTheory.Integrable
(data.pack.data.incomingExceptionalStopSourceDensity incomingMode (fun (omega : T4 × U) => omega.1)
fun (omega : T4 × U)
(v :
(data.pack.data.trace.stopPrefix.afterHead data.pack.data.terminal data.pack.data.suffix
⋯).SurvivingCoordinate →
T4) =>
charT4 outgoingMode omega.1 * coefficient omega.2
((data.outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv data.outgoing.terminalData.terminal [] ⋯)
(data.outgoing.endpoint.projection v)).2)
((paperMeasure.prod (paperMeasure.prod muU)).prod
(MeasureTheory.Measure.pi fun (x : data.pack.data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure)))
(hendpoint :
MeasureTheory.Integrable
(fun (q : (T4 × U) × (data.outgoing.endpoint.stop.SurvivingCoordinate → T4)) =>
data.outgoing.endpoint.stop.incomingPhasedResidualDensity
(data.outgoing.endpoint.multiplier incomingMode * (↑(paperSecondOrderModeDecay incomingMode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.pack.data.terminal.2) ⋯
data.pack.data.stopContext.internalEdges incomingMode * coefficient q.1.2
((data.outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv data.outgoing.terminalData.terminal [] ⋯)
q.2).2))
incomingMode rho eps 0 q.1.1 q.2)
((paperMeasure.prod muU).prod
(MeasureTheory.Measure.pi fun (x : data.outgoing.endpoint.stop.SurvivingCoordinate) => paperMeasure)))
(houtgoing :
∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.outgoing.terminalData.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.outgoing.terminalData.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.outgoing.terminalData.terminal.2) (↑kappaB)
data.outgoing.terminalContext.internalEdges
(primitiveAssemble (residualBlockOrder data.outgoing.terminalData.terminal.2) ⋯ first (first - gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.outgoing.terminalData.terminal.2 - 2)) =>
paperMeasure))
:
(R324PaperHalfEndpointUniformBound.ofExceptionalExceptional hsingles data).ExactTransform muU coefficient outgoingMode
The paper's complete exceptional/exceptional signed endpoint transform, with one arbitrary untouched parameter.
Equations
- One or more equations did not get rendered due to their size.