noncomputable def Anderson4D.PartialPairing.caseThreeVariablesEquiv (q r : ℕ) : (Fin (2 * (q + 1) + r) → T4) ≃ᵐ T4 × T4 × (Fin (2 * q + r) → T4)

The measurable coordinate permutation taking paper order (z,u,w,v) to the Fubini order (z,w,(u,v)).

Equations

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

theorem Anderson4D.PartialPairing.caseThreeVariablesEquiv_symm_apply (q r : ℕ) (z w : T4) (t : Fin (2 * q + r) → T4) : (caseThreeVariablesEquiv q r).symm (z, w, t) = caseThreeAmbientInternal q r z w t

The inverse coordinate permutation reconstructs the paper-order case-(3) internal tuple.

theorem Anderson4D.PartialPairing.measurePreserving_caseThreeVariablesEquiv (q r : ℕ) : MeasureTheory.MeasurePreserving (⇑(caseThreeVariablesEquiv q r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1) + r)) => paperMeasure) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure)))

The case-(3) coordinate permutation preserves the product of paper-normalized Haar measures.

theorem Anderson4D.PartialPairing.integral_caseThreeVariables (q r : ℕ) (f : (Fin (2 * (q + 1) + r) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1) + r)) => paperMeasure)) : (∫ (v : Fin (2 * (q + 1) + r) → T4), f v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1) + r)) => paperMeasure) = ∫ (z : T4), ∫ (w : T4), ∫ (t : Fin (2 * q + r) → T4), f (caseThreeAmbientInternal q r z w t) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure ∂paperMeasure ∂paperMeasure

Fubini after the case-(3) coordinate permutation (z,u,w,v) ↔ (z,w,(u,v)).

theorem Anderson4D.PartialPairing.caseThreeAmbientContribution_eq_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) (hint : MeasureTheory.Integrable (fun (v : Fin (2 * (q + 1) + r) → T4) => randIntegrand M ρ ε (σ.appendPairing τ) (assemble x y v) ω) (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1) + r)) => paperMeasure)) : caseThreeAmbientContribution M ρ lam ε q r σ τ x y ω = randRI M ρ lam ε (2 * (q + 1) + r) (σ.appendPairing τ) x y ω

The ambient case-(3) term is the existing random kernel for the appended prefix/tail pairing.

theorem Anderson4D.PartialPairing.caseThreeJointContribution_eq_randRI_add_delta (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (x y : T4) (ω : M.Ω) (hsplit : 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) (hambient : MeasureTheory.Integrable (fun (v : Fin (2 * (q + 1) + r) → T4) => randIntegrand M ρ ε (σ.appendPairing τ) (assemble x y v) ω) (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1) + r)) => paperMeasure)) : caseThreeJointContribution M ρ lam ε q r σ τ x y ω = randRI M ρ lam ε (2 * (q + 1) + r) (σ.appendPairing τ) x y ω + caseThreeDeltaContribution M ρ lam ε (q + 1) r σ τ x y ω

Fixed-pairing case-(3) identity. A non-split fully paired prefix contributes the ambient appended-pairing kernel plus the collapsed delta term.