Integrability of graded parametrix words

On every sample for which the mollified noise is continuous, the vertex factor of a graded resolvent word is bounded. Global Green-chain integrability therefore makes the complete word integrable jointly in both endpoints and all internal variables.

theorem Anderson4D.PartialPairing.measurable_renormWordWeight (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (d : ℕ) : Measurable fun (z : T4) => renormWordWeight M ρ lam ε d z ω

theorem Anderson4D.PartialPairing.continuous_renormWordWeight (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (d : ℕ) : Continuous fun (z : T4) => renormWordWeight M ρ lam ε d z ω

noncomputable def Anderson4D.PartialPairing.renormWordMultiplierContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (word : List ℕ) : C(Fin word.length → T4, ℂ)

The finite vertex multiplier of one graded word, packaged as a continuous map so its uniform bound is canonical.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.renormWordMultiplierContinuousMap_apply (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (word : List ℕ) (v : Fin word.length → T4) : (renormWordMultiplierContinuousMap M ρ lam ε ω hξ word) v = ∏ i : Fin word.length, ↑(renormWordWeight M ρ lam ε (word.get i) (v i) ω)

theorem Anderson4D.PartialPairing.integrable_renormWordIntegrandOnTuple_global (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (word : List ℕ) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin word.length → T4)) => ↑(renormWordIntegrandOnTuple M ρ lam ε word (assemble p.1 p.2.1 p.2.2) ω)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin word.length) => paperMeasure)))

Joint integrability of a complete graded word in flat coordinates. This is the global, coefficient-level analytic input for Proposition 3.4.

theorem Anderson4D.PartialPairing.ae_ae_renormWordIntegrable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (word : List ℕ) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, RenormWordIntegrable M ρ lam ε word x y ω

Consequently, the fixed-endpoint word ledger holds for almost every pair of external points. This is the section statement used by coefficient-level Fubini; no false assertion is made on the diagonal.

theorem Anderson4D.PartialPairing.ae_ae_gradedParametrix_succ_eq_noise_sub_counterterms (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (n : ℕ) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, gradedParametrix M ρ lam ε (n + 1) x y ω = gradedParametrixNoiseSource M ρ lam ε n x y ω - gradedOrderCountertermSum M ρ lam ε n x y ω

The graded Proposition 3.4 recurrence therefore holds almost everywhere in the two external variables on every continuous noise sample.