Exact signed transform interface for one paper endpoint half #
The four endpoint branches already have parameter-carrier identities. This file records only their common output: an arbitrary untouched parameter is left outside the completed signed half density. The source integral remains branch-literal; no norm, new integrability premise, or new Fubini theorem is introduced here.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.transformTarget
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{route : R324PaperHalfCompletedRoute pairing incomingMode}
(bound : R324PaperHalfEndpointUniformBound route)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
(coefficient : U → (bound.carrier.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
:
The signed parameter-carrier integral after one complete endpoint half. The outer parameter is untouched until both endpoint operations of the half have finished.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{route : R324PaperHalfCompletedRoute pairing incomingMode}
(bound : R324PaperHalfEndpointUniformBound route)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
(coefficient : U → (bound.carrier.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
:
A concrete application of one of the four existing parameterized signed
endpoint identities. source is deliberately branch-literal: DD/DE use
the ordinary initial residual source, while ED/EE use the incoming-head
source.
- source : ℂ
- exact_transform : ↑(lamEps lam eps) ^ (2 * (initial rho lam eps pairing).remainingOrder) * self.source = bound.transformTarget muU coefficient outgoingMode
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.compose
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{leftPairing rightPairing : PartialPairing (Fin m)}
{leftMode rightMode : Z4}
{leftRoute : R324PaperHalfCompletedRoute leftPairing leftMode}
{rightRoute : R324PaperHalfCompletedRoute rightPairing rightMode}
{leftBound : R324PaperHalfEndpointUniformBound leftRoute}
{rightBound : R324PaperHalfEndpointUniformBound rightRoute}
{UL : Type u_1}
{UR : Type u_2}
[MeasurableSpace UL]
[MeasurableSpace UR]
{muL : MeasureTheory.Measure UL}
{muR : MeasureTheory.Measure UR}
{leftCoefficient : UL → (leftBound.carrier.SurvivingCoordinate → T4) → ℂ}
{rightCoefficient : UR → (rightBound.carrier.SurvivingCoordinate → T4) → ℂ}
{leftOutgoingMode rightOutgoingMode : Z4}
(left : leftBound.ExactTransform muL leftCoefficient leftOutgoingMode)
(right : rightBound.ExactTransform muR rightCoefficient rightOutgoingMode)
(hsource : right.source = leftBound.transformTarget muL leftCoefficient leftOutgoingMode)
:
↑(lamEps lam eps) ^ (2 * ((initial rho lam eps leftPairing).remainingOrder + (initial rho lam eps rightPairing).remainingOrder)) * left.source = rightBound.transformTarget muR rightCoefficient rightOutgoingMode
Compose two already-proved signed half transforms. The sole interface
between them is equality of the second source with the first target; in the
paper applications this equality is the existing product-measure regroup.
The proof is only pow_add and reassociation.
Literal constructors from the four paper endpoint identities #
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.ofDirectDirect
{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 : R324PaperHalfDirectDirectRoute providers)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
[MeasureTheory.SFinite muU]
(coefficient : U → (data.transport.final.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(hcurrent :
MeasureTheory.Integrable
(fun (q : (T4 × U) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)) =>
(initial rho lam eps pairing).incomingPhasedResidualDensity
(charT4 outgoingMode q.1.1 * (↑(paperSecondOrderModeDecay incomingMode) * coefficient q.1.2 (data.transport.projection q.2)))
incomingMode rho eps 0 q.1.1 q.2)
((paperMeasure.prod muU).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure)))
(hedge : data.transport.final.state.edges (data.transport.final.terminalOutgoingEdgeSlot ⋯) = greenFn)
(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) * 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.ofDirectDirect houtgoing data).ExactTransform muU coefficient outgoingMode
The direct/direct instance is exactly the existing parameter-carrier identity, with the direct incoming Fourier decay left in its coefficient. No estimate or interchange of integrals is performed here.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.directExceptionalTarget
{rho : SmoothCutoff}
{lam eps : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
(outgoing : (initial rho lam eps pairing).R324PaperOutgoingEndpointTerminal)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
(coefficient : U → (outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
:
The direct/exceptional instance is the retained-terminal identity with the already evaluated direct incoming Fourier coefficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.directExceptionalTarget_transport
{rho : SmoothCutoff}
{lam eps : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{left right : (initial rho lam eps pairing).R324PaperOutgoingEndpointTerminal}
(h : left = right)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
(coefficient : U → (right.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
:
directExceptionalTarget left muU (fun (u : U) => ⋯.mp (coefficient u)) outgoingMode = directExceptionalTarget right muU coefficient outgoingMode
Transporting the terminal presentation transports its completed signed target and nothing else.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.directExceptionalGeometryCoefficient
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
{U : Type u_1}
(coefficient : U → (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
:
U → (data.geometry.paperOutgoingTerminal.terminalPost.SurvivingCoordinate → T4) → ℂ
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ExactTransform.ofDirectExceptional
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
{U : Type u_1}
[MeasurableSpace U]
(muU : MeasureTheory.Measure U)
[MeasureTheory.SFinite muU]
(coefficient : U → (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(hcurrent :
MeasureTheory.Integrable
(fun (q : U × T4 × ((initial rho lam eps pairing).SurvivingCoordinate → T4)) =>
(initial rho lam eps pairing).incomingPhasedResidualDensity
(directExceptionalGeometryCoefficient data coefficient q.1
((data.geometry.transport.stop.splitSurvivingPiMeasurableEquiv data.geometry.terminalData.terminal [] ⋯)
(data.geometry.transport.projection q.2.2)).2)
incomingMode rho eps 0 q.2.1 q.2.2)
(muU.prod
(paperMeasure.prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure))))
(hstop :
MeasureTheory.Integrable
(fun (q : U × T4 × (data.geometry.transport.stop.SurvivingCoordinate → T4)) =>
data.geometry.transport.stop.incomingPhasedResidualDensity
(data.geometry.transport.multiplier incomingMode * directExceptionalGeometryCoefficient data coefficient q.1
((data.geometry.transport.stop.splitSurvivingPiMeasurableEquiv data.geometry.terminalData.terminal [] ⋯)
q.2.2).2)
incomingMode rho eps 0 q.2.1 q.2.2)
(muU.prod
(paperMeasure.prod
(MeasureTheory.Measure.pi fun (x : data.geometry.transport.stop.SurvivingCoordinate) => paperMeasure))))
(hint :
∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.geometry.terminalData.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.geometry.terminalData.terminal.2) (↑kappaB)
data.geometry.paperOutgoingTerminal.terminalContext.internalEdges
(primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ first (first - gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) =>
paperMeasure))
:
(R324PaperHalfEndpointUniformBound.ofDirectExceptional data).ExactTransform muU coefficient outgoingMode
Equations
- One or more equations did not get rendered due to their size.