Measurability of random parametrix coefficients

The coefficient-level resolvent route uses totalized Bochner integrals and tsum. This file proves that these totalizations remain measurable in the noise sample. In particular, no measurability is hidden in the good-event replacement step.

theorem Anderson4D.NoiseModel.measurable_multFun_joint (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable fun (p : M.Ω × T4) => multFun M ρ lam ε p.2 p.1

The random multiplication potential is jointly measurable in the sample and spatial point.

noncomputable def Anderson4D.neumannRawIntegrand (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (α β : Z4) (ω : M.Ω) (x y : T4) (v : Fin n → T4) : ℂ

The unintegrated coefficient-chain integrand.

Equations

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

theorem Anderson4D.measurable_neumannRawIntegrand (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (α β : Z4) : Measurable fun (p : ((M.Ω × T4) × T4) × (Fin n → T4)) => neumannRawIntegrand M ρ lam ε n α β p.1.1.1 p.1.1.2 p.1.2 p.2

Joint measurability of the complete unintegrated Neumann coefficient chain.

theorem Anderson4D.measurable_neumannCoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (α β : Z4) : Measurable (neumannCoeff M ρ lam ε n α β)

Each totalized Neumann coefficient is measurable in the noise sample.

theorem Anderson4D.measurable_modeHcoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) : Measurable (modeHcoeff M ρ lam ε α β)

The totalized Neumann tail is measurable.