Physical Fubini at an exceptional incoming R-324 stop

This module performs only the endpoint Fubini step at a certified stop immediately before an exceptional incoming head. The consumed prefix is not treated here, and the retained head and its complete suffix are not absorbed.

The source density is jointly integrable in the incoming endpoint, an arbitrary measured parameter, and the genuine stop coordinates. The stop coordinates are split into the retained head tuple and the after-head surviving tuple. Fubini then puts the incoming endpoint on the inside, where the pre-collapse Fourier identity applies while the incoming edge is still the free Green kernel.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalStopSourceDensity {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (p : (T4 × Ω) × (data.trace.stopPrefix.SurvivingCoordinate → T4)) : ℂ

The signed stop density before the incoming endpoint is integrated. The arbitrary outer factor lives only on the genuine after-head surviving coordinates and on the measured parameter.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalStopFourierDensity {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (p : Ω × (Fin (2 * residualBlockOrder data.terminal.2) → T4) × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)) : ℂ

The density after the incoming endpoint integral has been evaluated. The retained head tuple and the after-head coordinates are both still present; in particular this definition performs no head collapse.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integral_incomingExceptionalStop_splitSection_eq {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (ω : Ω) (t : Fin (2 * residualBlockOrder data.terminal.2) → T4) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : ∫ (x : T4), ↑(data.trace.stopPrefix.residualIntegrand ρ ε x (y ω) (data.trace.stopPrefix.reconstruct ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯).symm (t, v)))) * (charT4 k x * postOuter ω v) ∂paperMeasure = data.incomingExceptionalStopFourierDensity k y postOuter (ω, t, v)

Pointwise inner-endpoint evaluation after the genuine stop-coordinate split. This is the analytic heart of the global Fubini theorem below.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalStopFourierDensity {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.SFinite ν] (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity k y postOuter) ((paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (data.incomingExceptionalStopFourierDensity k y postOuter) (ν.prod ((MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure)))

Joint integrability of the exact stop density licenses the endpoint-first Fubini order. After the genuine stop coordinates are split, the incoming endpoint is integrated out and the retained head and complete post tuple remain as jointly integrable variables.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integral_incomingExceptionalStopSourceDensity_eq_fourierDensity {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.SFinite ν] (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity k y postOuter) ((paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) : ∫ (p : (T4 × Ω) × (data.trace.stopPrefix.SurvivingCoordinate → T4)), data.incomingExceptionalStopSourceDensity k y postOuter p ∂(paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure) = ∫ (p : Ω × (Fin (2 * residualBlockOrder data.terminal.2) → T4) × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)), data.incomingExceptionalStopFourierDensity k y postOuter p ∂ν.prod ((MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure))

Exact product-space Fubini identity at an exceptional incoming stop. The retained head tuple and the complete post tuple remain outside the incoming endpoint integral, with no collapse or trace weight applied.