Minimal hypotheses for linearity of three nested totalized integrals

structure Anderson4D.PartialPairing.NestedIntegrablePair3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μα : MeasureTheory.Measure α) (μβ : MeasureTheory.Measure β) (μγ : MeasureTheory.Measure γ) (left right : α → β → γ → ℝ) : Prop

The six exact integrability conditions needed to distribute three nested Bochner integrals over left + right.

They are deliberately stated at the nesting levels at which MeasureTheory.integral_add is used:

• both innermost integrands are integrable almost everywhere in (x,y);
• both resulting middle integrands are integrable almost everywhere in x;
• both resulting outer integrands are integrable.

• left_inner : ∀ᵐ (x : α) ∂μα, ∀ᵐ (y : β) ∂μβ, MeasureTheory.Integrable (left x y) μγ
• right_inner : ∀ᵐ (x : α) ∂μα, ∀ᵐ (y : β) ∂μβ, MeasureTheory.Integrable (right x y) μγ
• left_middle : ∀ᵐ (x : α) ∂μα, MeasureTheory.Integrable (fun (y : β) => ∫ (z : γ), left x y z ∂μγ) μβ
• right_middle : ∀ᵐ (x : α) ∂μα, MeasureTheory.Integrable (fun (y : β) => ∫ (z : γ), right x y z ∂μγ) μβ
• left_outer : MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), ∫ (z : γ), left x y z ∂μγ ∂μβ) μα
• right_outer : MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), ∫ (z : γ), right x y z ∂μγ ∂μβ) μα

theorem Anderson4D.PartialPairing.integral3_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μα : MeasureTheory.Measure α} {μβ : MeasureTheory.Measure β} {μγ : MeasureTheory.Measure γ} {left right : α → β → γ → ℝ} (h : NestedIntegrablePair3 μα μβ μγ left right) : ∫ (x : α), ∫ (y : β), ∫ (z : γ), left x y z + right x y z ∂μγ ∂μβ ∂μα = ∫ (x : α), ∫ (y : β), ∫ (z : γ), left x y z ∂μγ ∂μβ ∂μα + ∫ (x : α), ∫ (y : β), ∫ (z : γ), right x y z ∂μγ ∂μβ ∂μα

Pointwise ambient and diagonal pieces

noncomputable def Anderson4D.PartialPairing.caseThreeAmbientCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x z w y : T4) (ω : M.Ω) (t : Fin (2 * q + r) → T4) : ℝ

Equations

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

noncomputable def Anderson4D.PartialPairing.caseThreeDiagonalCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x z w y : T4) (ω : M.Ω) (t : Fin (2 * q + r) → T4) : ℝ

Equations

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

noncomputable def Anderson4D.PartialPairing.caseThreeAmbientContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : ℝ

Equations

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

noncomputable def Anderson4D.PartialPairing.caseThreeDiagonalContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : ℝ

Equations

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

theorem Anderson4D.PartialPairing.caseThreeJointContribution_eq_ambient_add_diagonal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x y : T4) (ω : M.Ω) (hint : NestedIntegrablePair3 paperMeasure paperMeasure (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure) (fun (z w : T4) (t : Fin (2 * q + r) → T4) => caseThreeAmbientCore M ρ ε q r σ τ x z w y ω t) fun (z w : T4) (t : Fin (2 * q + r) → T4) => caseThreeDiagonalCore M ρ ε q r σ τ x z w y ω t) : caseThreeJointContribution M ρ lam ε q r σ τ x y ω = caseThreeAmbientContribution M ρ lam ε q r σ τ x y ω + caseThreeDiagonalContribution M ρ lam ε q r σ τ x y ω

theorem Anderson4D.PartialPairing.setTupleFirst_caseThreeTailTuple (q r : ℕ) (z w y : T4) (t : Fin (2 * q + r) → T4) : setTupleFirst z (caseThreeTailTuple q r w y t) = assemble z y fun (j : Fin r) => t (Fin.natAdd (2 * q) j)

noncomputable def Anderson4D.PartialPairing.caseThreeDiagonalJointCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (z w y : T4) (ω : M.Ω) (t : Fin (2 * q + r) → T4) : ℝ

The separated diagonal core without the outer Green factor.

Equations

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

theorem Anderson4D.PartialPairing.caseThreeDiagonalCore_eq (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x z w y : T4) (ω : M.Ω) (t : Fin (2 * q + r) → T4) : caseThreeDiagonalCore M ρ ε q r σ τ x z w y ω t = greenFn (x - z) * caseThreeDiagonalJointCore M ρ ε q r σ τ z w y ω t

theorem Anderson4D.PartialPairing.integral_caseThreeDiagonalJointCore_eq_mul (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (z w y : T4) (ω : M.Ω) : (∫ (t : Fin (2 * q + r) → T4), caseThreeDiagonalJointCore M ρ ε q r σ τ z w y ω t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure) = (∫ (u : Fin (2 * q) → T4), detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure) * ∫ (v : Fin r → T4), randIntegrand M ρ ε τ (assemble z y v) ω ∂MeasureTheory.Measure.pi fun (x : Fin r) => paperMeasure

Finite-product Fubini for the diagonal summand.

theorem Anderson4D.PartialPairing.integral_caseThreeDiagonalCore_eq_mul (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x z w y : T4) (ω : M.Ω) : (∫ (t : Fin (2 * q + r) → T4), caseThreeDiagonalCore M ρ ε q r σ τ x z w y ω t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure) = greenFn (x - z) * ((∫ (u : Fin (2 * q) → T4), detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure) * ∫ (v : Fin r → T4), randIntegrand M ρ ε τ (assemble z y v) ω ∂MeasureTheory.Measure.pi fun (x : Fin r) => paperMeasure)

The same factorization with the outer Green factor restored.

theorem Anderson4D.PartialPairing.caseThreeDiagonalContribution_eq_delta (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : caseThreeDiagonalContribution M ρ lam ε q r σ τ x y ω = caseThreeDeltaContribution M ρ lam ε (q + 1) r σ τ x y ω

The joint-coordinate diagonal contribution is exactly the existing collapsed-delta contribution.

theorem Anderson4D.PartialPairing.caseThreeJointContribution_eq_ambient_add_delta (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x y : T4) (ω : M.Ω) (hint : NestedIntegrablePair3 paperMeasure paperMeasure (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure) (fun (z w : T4) (t : Fin (2 * q + r) → T4) => caseThreeAmbientCore M ρ ε q r σ τ x z w y ω t) fun (z w : T4) (t : Fin (2 * q + r) → T4) => caseThreeDiagonalCore M ρ ε q r σ τ x z w y ω t) : caseThreeJointContribution M ρ lam ε q r σ τ x y ω = caseThreeAmbientContribution M ρ lam ε q r σ τ x y ω + caseThreeDeltaContribution M ρ lam ε (q + 1) r σ τ x y ω

Integrated case-(3) split, paper (3.18)–(3.19). Under exactly the six nested integrability conditions needed for linearity of the three iterated Bochner integrals, the raw joint contribution is the ambient renormalized contribution plus the paper's existing collapsed delta contribution.