Exact signed transform adapter for the paper ED endpoint half #
This file only exposes the already proved single-parameter exceptional-incoming/direct-outgoing identity through the common endpoint interface. In particular, the incoming exceptional head and the outgoing Fourier leg are both evaluated before the common target is formed; no norm or new estimate occurs here.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.ofExceptionalDirect
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(houtgoing : Fin.last m ∉ extractedRightEdges pairing)
(data : R324PaperHalfExceptionalDirectRoute providers)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
[MeasureTheory.SFinite muU]
(coefficient : U → (data.transport.final.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(hG :
∀ (j : Fin (2 * residualBlockOrder data.pack.data.stopContext.step.2 - 1)),
MemEClassT4 (data.pack.data.stopContext.internalEdges j))
(hint :
∀ (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.transport.projection v))
((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.transport.projection v))
((paperMeasure.prod (paperMeasure.prod muU)).prod
(MeasureTheory.Measure.pi fun (x : data.pack.data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure)))
(hterminal :
MeasureTheory.Integrable
(fun (q : (T4 × U) × (data.transport.final.SurvivingCoordinate → T4)) =>
data.transport.final.incomingPhasedResidualDensity
(charT4 outgoingMode q.1.1 * (data.transport.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 q.2)))
incomingMode rho eps 0 q.1.1 q.2)
((paperMeasure.prod muU).prod
(MeasureTheory.Measure.pi fun (x : data.transport.final.SurvivingCoordinate) => paperMeasure)))
:
(R324PaperHalfEndpointUniformBound.ofExceptionalDirect houtgoing data).ExactTransform muU coefficient outgoingMode
The exceptional/direct common-interface instance is exactly the existing single-parameter signed endpoint identity. All analytic premises are kept literal so this adapter performs no hidden interchange or estimate.
Equations
- One or more equations did not get rendered due to their size.