Outer Fubini for one processed R-324 within-half step

An arbitrary fixed outer factor passes through the current block integral. The almost-everywhere wrapper then performs the exact outer-measure substitution from the raw local factor to the absorbed predecessor edge.

theorem Anderson4D.R324WithinHalfStepContext.rawLocalSpatialIntegral_mul_outer_eq_absorb {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) (outer : ℝ) (hstandard : MeasureTheory.Integrable (ctx.localIntegrand ρ ε u) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder ctx.step.2) * ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ctx.rawLocalIntegrand ρ ε u t * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) = (ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) u * outer

One processed inner integral may carry any fixed outer factor.

theorem Anderson4D.R324WithinHalfStepContext.integral_outer_rawLocalIntegrand_eq_absorb {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (ρ : SmoothCutoff) (lam ε : ℝ) (u : Ω → T4) (outer : Ω → ℝ) (hstandard : ∀ᵐ (ω : Ω) ∂ν, MeasureTheory.Integrable (ctx.localIntegrand ρ ε (u ω)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : ∫ (ω : Ω), lamEps lam ε ^ (2 * residualBlockOrder ctx.step.2) * ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ctx.rawLocalIntegrand ρ ε (u ω) t * outer ω ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure ∂ν = ∫ (ω : Ω), (ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (u ω) * outer ω ∂ν

Exact outer-Fubini substitution for a genuine processed step. Section integrability is required only almost everywhere in the actual outer coordinate.