Almost-everywhere coefficient closure for Proposition 3.4 #
The global integrability results give endpoint sections in either Fubini
order. The right-endpoint-first order is the one needed by the strong
induction in the parametrix recurrence: after fixing y, the preceding
order is substituted under the z integral.
No almost-everywhere quantifiers are commuted abstractly here. Instead,
the underlying jointly integrable functions are transported by the
measure-preserving permutation (x,y,v) ↦ (y,x,v) before Fubini is
applied.
A measure-preserving endpoint permutation #
def
Anderson4D.PartialPairing.moveMiddleMeasurableEquiv
(A : Type u_1)
(B : Type u_2)
(C : Type u_3)
[MeasurableSpace A]
[MeasurableSpace B]
[MeasurableSpace C]
:
Move the middle coordinate of a right-associated product to the front.
Equations
Instances For
theorem
Anderson4D.PartialPairing.measurePreserving_moveMiddleMeasurableEquiv
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
[MeasurableSpace A]
[MeasurableSpace B]
[MeasurableSpace C]
(μ : MeasureTheory.Measure A)
(ν : MeasureTheory.Measure B)
(τ : MeasureTheory.Measure C)
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite τ]
:
MeasureTheory.MeasurePreserving (⇑(moveMiddleMeasurableEquiv A B C)) (μ.prod (ν.prod τ)) (ν.prod (μ.prod τ))
theorem
Anderson4D.PartialPairing.integrable_moveMiddle
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
{E : Type u_4}
[MeasurableSpace A]
[MeasurableSpace B]
[MeasurableSpace C]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure A}
{ν : MeasureTheory.Measure B}
{τ : MeasureTheory.Measure C}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite τ]
(f : A → B → C → E)
(hf : MeasureTheory.Integrable (fun (p : A × B × C) => f p.1 p.2.1 p.2.2) (μ.prod (ν.prod τ)))
:
MeasureTheory.Integrable (fun (p : B × A × C) => f p.2.1 p.1 p.2.2) (ν.prod (μ.prod τ))
Right-endpoint-first pairing sections #
theorem
Anderson4D.PartialPairing.ae_ae_integrable_randIntegrand_all_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(m : ℕ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, ∀ (κ : PartialPairing (Fin m)),
MeasureTheory.Integrable (fun (v : Fin m → T4) => ↑(randIntegrand M ρ ε κ (assemble x y v) ω))
(MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)
The global random-pairing profile gives its internal-variable integrability with the right endpoint quantified first.
theorem
Anderson4D.PartialPairing.ae_ae_integrable_leftRankedContractionWeightedCore_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(n : ℕ)
(κ : PartialPairing (Fin n))
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, ∀ (j : Fin κ.singles.card),
MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => leftRankedContractionWeightedCore M ρ ε κ j x p.1 y p.2 ω)
(paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))
Every ranked Wick contraction has the same right-endpoint-first sections.
theorem
Anderson4D.PartialPairing.ae_ae_leftPairingSplitIntegrability_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(n : ℕ)
(κ : PartialPairing (Fin n))
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, LeftPairingSplitIntegrability M ρ ε n κ x y ω
The complete fixed-pairing Wick split is available in the right-endpoint-first Fubini order.
theorem
Anderson4D.PartialPairing.ae_ae_leftOrderSourceIntegrability_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(n : ℕ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, LeftOrderSourceIntegrability M ρ lam ε n x y ω
The finite old-pairing source ledger is available with y
quantified first.
theorem
Anderson4D.PartialPairing.ae_ae_integrable_leftMarkedContractionWeightedCore_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
{n : ℕ}
(d : MarkedSingle (Fin n))
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => leftMarkedContractionWeightedCore M ρ ε d x p.1 y p.2 ω)
(paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))
Directly marked contractions inherit the right-endpoint-first sections from their ranked presentation.
theorem
Anderson4D.PartialPairing.ae_ae_integrable_green_mul_randRI_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(r : ℕ)
(τ : PartialPairing (Fin r))
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * randRI M ρ lam ε r τ z y ω) paperMeasure
The free Green convolution of one pairing profile also has right-endpoint-first sections.
Right-endpoint-first case-(3) ledgers #
theorem
Anderson4D.PartialPairing.caseThreeSummationIntegrability_fixed_of_local
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(q r : ℕ)
(σ : PartialPairing (Fin (2 * (q + 1))))
(τ : PartialPairing (Fin r))
(hσ : IsNonSplit σ)
(x y : T4)
(ω : M.Ω)
(hambientComplex :
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))
(hcontraction :
MeasureTheory.Integrable
(fun (p : T4 × (Fin (2 * q + 1 + r) → T4)) =>
leftMarkedContractionWeightedCore M ρ ε (caseThreeHeadDeletionData q r σ τ hσ) x p.1 y p.2 ω)
(paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure)))
(hfree : MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * randRI M ρ lam ε r τ z y ω) paperMeasure)
:
(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) ∧ 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) ∧ MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * detJMass ρ lam ε (q + 1) σ * randRI M ρ lam ε r τ z y ω)
paperMeasure
Local jointly integrable data imply the three fixed-prefix case-(3) summation fields.
theorem
Anderson4D.PartialPairing.ae_ae_caseThreeSummationIntegrability_fixed_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(q r : ℕ)
(σ : PartialPairing (Fin (2 * (q + 1))))
(τ : PartialPairing (Fin r))
(hσ : IsNonSplit σ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, (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) ∧ 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) ∧ MeasureTheory.Integrable
(fun (z : T4) => greenFn (x - z) * detJMass ρ lam ε (q + 1) σ * randRI M ρ lam ε r τ z y ω) paperMeasure
One fixed case-(3) prefix/tail pair has all summation fields in the right-endpoint-first order.
theorem
Anderson4D.PartialPairing.ae_ae_caseThreeSummationIntegrability_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(q r : ℕ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, CaseThreeSummationIntegrability M ρ lam ε q r x y ω
The complete finite summation ledger is simultaneous in the right-endpoint-first order.
theorem
Anderson4D.PartialPairing.ae_ae_caseThreeHeadContractionIntegrability_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(q r : ℕ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, CaseThreeHeadContractionIntegrability M ρ ε q r x y ω
The actual marked head contractions used by case (3) are simultaneous in the right-endpoint-first order.
theorem
Anderson4D.PartialPairing.ae_ae_leftWithPrefixCaseThreeIntegrability_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(n : ℕ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, LeftWithPrefixCaseThreeIntegrability M ρ lam ε n x y ω
Every minimal-prefix case-(3) ledger at one order is simultaneous in the right-endpoint-first order.
Right-endpoint-first graded recurrence #
theorem
Anderson4D.PartialPairing.ae_ae_renormWordIntegrable_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
(word : List ℕ)
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, RenormWordIntegrable M ρ lam ε word x y ω
theorem
Anderson4D.PartialPairing.ae_ae_gradedParametrix_succ_eq_noise_sub_counterterms_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
(n : ℕ)
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, gradedParametrix M ρ lam ε (n + 1) x y ω = gradedParametrixNoiseSource M ρ lam ε n x y ω - gradedOrderCountertermSum M ρ lam ε n x y ω
Strong induction for the pairing/graded comparison #
theorem
Anderson4D.PartialPairing.ae_ae_parametrixP_eq_gradedParametrix_rightFirst
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
(n : ℕ)
:
∀ᵐ (y : T4) (x : T4) ∂paperMeasure, parametrixP M ρ lam ε n x y ω = gradedParametrix M ρ lam ε n x y ω
On every continuous sample, the paper pairing expansion and the graded word expansion agree with the right endpoint quantified first. This is the Fubini orientation needed to substitute the induction hypothesis under the source and counterterm convolutions.
theorem
Anderson4D.PartialPairing.ae_ae_parametrixP_eq_gradedParametrix
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
(order : ℕ)
:
∀ᵐ (x : T4) (y : T4) ∂paperMeasure, parametrixP M ρ lam ε order x y ω = gradedParametrix M ρ lam ε order x y ω
The same equality in the paper's coefficient-integration order.
The preceding right-first theorem supplies every lower-order equality
under the z convolutions, so no interchange of abstract a.e.
quantifiers is used.
theorem
Anderson4D.PartialPairing.parametrixGradedCoefficientAgreement_of_continuous
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(A : ℕ)
(ω : M.Ω)
(hξ : Continuous (M.xiEps ρ ε ω))
:
ParametrixGradedCoefficientAgreement M ρ lam ε A ω
Proposition 3.4 now supplies the exact integrated coefficient
agreement required by the physical L² bridge on every continuous
sample.
theorem
Anderson4D.PartialPairing.ae_parametrixGradedCoefficientAgreement
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam : ℝ)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(A : ℕ)
:
∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω
The agreement is automatic on the full-measure event of continuous mollified-noise samples.