Measurable random multiplication operators

This file refines the samplewise construction in L2Realization.lean. The mollified Fourier series is summed in the separable Banach space of continuous functions on the compact torus. Continuous functions then map continuously to multiplication operators on L². Consequently the random potential and K = G M are honest strongly measurable operator-valued random variables, rather than merely a.e.-defined samplewise operators.

@[implicit_reducible]

noncomputable instance Anderson4D.instMeasurableSpaceContinuousMapT4 : MeasurableSpace C(T4, ℂ)

Equations

• Anderson4D.instMeasurableSpaceContinuousMapT4 = borel C(Anderson4D.T4, ℂ)

instance Anderson4D.instBorelSpaceContinuousMapT4 : BorelSpace C(T4, ℂ)

@[implicit_reducible]

noncomputable instance Anderson4D.instMeasurableSpaceTorusL2Operator : MeasurableSpace (↥TorusL2 →L[ℂ] ↥TorusL2)

Equations

• Anderson4D.instMeasurableSpaceTorusL2Operator = borel (↥Anderson4D.TorusL2 →L[ℂ] ↥Anderson4D.TorusL2)

instance Anderson4D.instBorelSpaceTorusL2Operator : BorelSpace (↥TorusL2 →L[ℂ] ↥TorusL2)

Continuous functions act continuously on L²

noncomputable def Anderson4D.continuousMultiplicationOp (m : C(T4, ℂ)) : ↥TorusL2 →L[ℂ] ↥TorusL2

Multiplication by a continuous torus function.

Equations

• Anderson4D.continuousMultiplicationOp m = Anderson4D.boundedMultiplicationCLM ⇑m ‖m‖ ⋯ ⋯ ⋯

@[simp]

theorem Anderson4D.continuousMultiplicationOp_apply_ae (m : C(T4, ℂ)) (f : ↥TorusL2) : ↑↑((continuousMultiplicationOp m) f) =ᵐ[haarT4] fun (x : T4) => m x * ↑↑f x

theorem Anderson4D.continuousMultiplicationOp_norm_le (m : C(T4, ℂ)) : ‖continuousMultiplicationOp m‖ ≤ ‖m‖

noncomputable def Anderson4D.continuousMultiplicationLM : C(T4, ℂ) →ₗ[ℂ] ↥TorusL2 →L[ℂ] ↥TorusL2

Linearity of the continuous-function multiplication construction.

Equations

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

noncomputable def Anderson4D.continuousMultiplicationCLM : C(T4, ℂ) →L[ℂ] ↥TorusL2 →L[ℂ] ↥TorusL2

Continuous dependence of the L² multiplication operator on its continuous multiplier.

Equations

• Anderson4D.continuousMultiplicationCLM = Anderson4D.continuousMultiplicationLM.mkContinuous 1 Anderson4D.continuousMultiplicationCLM._proof_2

@[simp]

theorem Anderson4D.continuousMultiplicationCLM_apply (m : C(T4, ℂ)) : continuousMultiplicationCLM m = continuousMultiplicationOp m

theorem Anderson4D.continuousMultiplicationCLM_norm_le_one : ‖continuousMultiplicationCLM‖ ≤ 1

A continuous-map version of the mollified Fourier series

theorem Anderson4D.norm_charT4Continuous (k : Z4) : ‖charT4Continuous k‖ = 1

noncomputable def Anderson4D.mollifiedNoiseContinuousTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) (ω : M.Ω) : C(T4, ℂ)

One continuous-function-valued Fourier summand of the mollified noise.

Equations

• Anderson4D.mollifiedNoiseContinuousTerm M ρ ε k ω = (↑Anderson4D.NoiseModel.whiteNoiseFourierScale * M.mollifiedRandomCoeff ρ ε k ω) • Anderson4D.charT4Continuous k

theorem Anderson4D.measurable_mollifiedNoiseContinuousTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : Measurable (mollifiedNoiseContinuousTerm M ρ ε k)

theorem Anderson4D.norm_mollifiedNoiseContinuousTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) (ω : M.Ω) : ‖mollifiedNoiseContinuousTerm M ρ ε k ω‖ = ‖NoiseModel.whiteNoiseFourierScale‖ * ‖M.mollifiedRandomCoeff ρ ε k ω‖

noncomputable def Anderson4D.xiEpsContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) : C(T4, ℂ)

Canonical continuous-function-valued mollified noise. The Banach space tsum is zero off summability, giving a measurable totalization that agrees with xiEps almost surely at every positive scale.

Equations

• Anderson4D.xiEpsContinuousMap M ρ ε ω = ∑' (k : Anderson4D.Z4), Anderson4D.mollifiedNoiseContinuousTerm M ρ ε k ω

theorem Anderson4D.measurable_xiEpsContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) : Measurable (xiEpsContinuousMap M ρ ε)

theorem Anderson4D.summable_mollifiedNoiseContinuousTerm_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) : Summable fun (k : Z4) => mollifiedNoiseContinuousTerm M ρ ε k ω

theorem Anderson4D.xiEpsContinuousMap_apply_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (x : T4) : (xiEpsContinuousMap M ρ ε ω) x = ↑NoiseModel.whiteNoiseFourierScale * ∑' (k : Z4), M.mollifiedRandomCoeff ρ ε k ω * charT4 k x

theorem Anderson4D.xiEpsContinuousMap_re_eq_xiEps_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (x : T4) : ((xiEpsContinuousMap M ρ ε ω) x).re = M.xiEps ρ ε ω x

theorem Anderson4D.xiEpsContinuousMap_eq_xiEps_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (x : T4) : (xiEpsContinuousMap M ρ ε ω) x = ↑(M.xiEps ρ ε ω x)

theorem Anderson4D.ae_forall_xiEpsContinuousMap_re_eq_xiEps (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), ∀ (x : T4), ((xiEpsContinuousMap M ρ ε ω) x).re = M.xiEps ρ ε ω x

At positive scale the continuous-map totalization agrees with the original scalar Fourier-series definition, simultaneously at all torus points.

Measurable random potential and K

noncomputable def Anderson4D.measurableMollifiedPotential (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : C(T4, ℂ)

The continuous-map-valued Anderson potential. Its Banach tsum totalization is measurable for every sample and agrees a.s. with multFun at positive scale.

Equations

• Anderson4D.measurableMollifiedPotential M ρ lam ε ω = ↑(Anderson4D.lamEps lam ε) • Anderson4D.xiEpsContinuousMap M ρ ε ω - ContinuousMap.const Anderson4D.T4 ↑(Anderson4D.renormCEps ρ lam ε)

theorem Anderson4D.measurable_measurableMollifiedPotential (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable (measurableMollifiedPotential M ρ lam ε)

theorem Anderson4D.measurableMollifiedPotential_apply_eq_multFun_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (x : T4) : (measurableMollifiedPotential M ρ lam ε ω) x = ↑(multFun M ρ lam ε x ω)

noncomputable def Anderson4D.measurableMollifiedPotentialL2Op (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

Preferred measurable multiplication-operator realization of the mollified potential.

Equations

• Anderson4D.measurableMollifiedPotentialL2Op M ρ lam ε ω = Anderson4D.continuousMultiplicationCLM (Anderson4D.measurableMollifiedPotential M ρ lam ε ω)

theorem Anderson4D.measurable_measurableMollifiedPotentialL2Op (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable (measurableMollifiedPotentialL2Op M ρ lam ε)

theorem Anderson4D.measurableMollifiedPotentialL2Op_apply_ae_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (f : ↥TorusL2) : ↑↑((measurableMollifiedPotentialL2Op M ρ lam ε ω) f) =ᵐ[haarT4] fun (x : T4) => ↑(multFun M ρ lam ε x ω) * ↑↑f x

noncomputable def Anderson4D.measurableAndersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

The measurable random bounded operator Kε = G ∘ Mε.

Equations

• Anderson4D.measurableAndersonK M ρ lam ε ω = Anderson4D.Kop Anderson4D.greenL2Op (Anderson4D.measurableMollifiedPotentialL2Op M ρ lam ε ω)

theorem Anderson4D.measurable_measurableAndersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable (measurableAndersonK M ρ lam ε)

theorem Anderson4D.measurable_norm_sq_measurableAndersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable fun (ω : M.Ω) => ‖measurableAndersonK M ρ lam ε ω‖ ^ 2

Quantitative L²(Ω) control

noncomputable def Anderson4D.noiseCoeffLp (M : NoiseModel) (k : Z4) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

A noise Fourier coefficient as an element of L²(Ω; ℂ).

Equations

• Anderson4D.noiseCoeffLp M k = MeasureTheory.MemLp.toLp (M.g k) ⋯

theorem Anderson4D.norm_noiseCoeffLp (M : NoiseModel) (k : Z4) : ‖noiseCoeffLp M k‖ = 1

theorem Anderson4D.memLp_mollifiedNoiseContinuousTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : MeasureTheory.MemLp (mollifiedNoiseContinuousTerm M ρ ε k) 2 MeasureTheory.volume

Each continuous Fourier summand has the expected L²(Ω) bound.

noncomputable def Anderson4D.mollifiedNoiseContinuousTermLp (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ↥(MeasureTheory.Lp C(T4, ℂ) 2 MeasureTheory.volume)

One continuous Fourier summand in L²(Ω; C(𝕋⁴)).

Equations

• Anderson4D.mollifiedNoiseContinuousTermLp M ρ ε k = MeasureTheory.MemLp.toLp (Anderson4D.mollifiedNoiseContinuousTerm M ρ ε k) ⋯

theorem Anderson4D.norm_mollifiedNoiseContinuousTermLp_le (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖mollifiedNoiseContinuousTermLp M ρ ε k‖ ≤ ‖NoiseModel.whiteNoiseFourierScale‖ * ‖ρ.symbol ε k‖

theorem Anderson4D.summable_mollifiedNoiseContinuousTermLp (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : Summable fun (k : Z4) => mollifiedNoiseContinuousTermLp M ρ ε k

The continuous Fourier series is summable in L²(Ω), with the deterministic sum of cutoff symbols as a norm majorant.

noncomputable def Anderson4D.xiEpsContinuousMapLp (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) : ↥(MeasureTheory.Lp C(T4, ℂ) 2 MeasureTheory.volume)

The mollified continuous field as an L²(Ω; C(𝕋⁴)) random variable.

Equations

• Anderson4D.xiEpsContinuousMapLp M ρ ε = ∑' (k : Anderson4D.Z4), Anderson4D.mollifiedNoiseContinuousTermLp M ρ ε k

theorem Anderson4D.ae_xiEpsContinuousMapLp_eq (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ↑↑(xiEpsContinuousMapLp M ρ ε) =ᵐ[MeasureTheory.volume] xiEpsContinuousMap M ρ ε

theorem Anderson4D.norm_xiEpsContinuousMapLp_le (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ‖xiEpsContinuousMapLp M ρ ε‖ ≤ ‖NoiseModel.whiteNoiseFourierScale‖ * ∑' (k : Z4), ‖ρ.symbol ε k‖

theorem Anderson4D.memLp_xiEpsContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.MemLp (xiEpsContinuousMap M ρ ε) 2 MeasureTheory.volume

The measurable continuous-map totalization belongs to L²(Ω).

theorem Anderson4D.norm_sq_toLp_two_eq_integral_norm_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} (hf : MeasureTheory.MemLp f 2 μ) : ‖MeasureTheory.MemLp.toLp f hf‖ ^ 2 = ∫ (x : α), ‖f x‖ ^ 2 ∂μ

The squared L² norm of a strongly measurable representative is its second moment. This small adapter avoids repeatedly unfolding the real-valued lpNorm.

theorem Anderson4D.xiEpsContinuousMapLp_eq_toLp (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : xiEpsContinuousMapLp M ρ ε = MeasureTheory.MemLp.toLp (xiEpsContinuousMap M ρ ε) ⋯

theorem Anderson4D.integral_norm_sq_xiEpsContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∫ (ω : M.Ω), ‖xiEpsContinuousMap M ρ ε ω‖ ^ 2 = ‖xiEpsContinuousMapLp M ρ ε‖ ^ 2

Exact identification of the continuous field's second moment with the squared norm of its canonical L² sum.

theorem Anderson4D.integrable_norm_sq_xiEpsContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖xiEpsContinuousMap M ρ ε ω‖ ^ 2) MeasureTheory.volume

theorem Anderson4D.integral_norm_sq_xiEpsContinuousMap_le (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∫ (ω : M.Ω), ‖xiEpsContinuousMap M ρ ε ω‖ ^ 2 ≤ (‖NoiseModel.whiteNoiseFourierScale‖ * ∑' (k : Z4), ‖ρ.symbol ε k‖) ^ 2

A fully explicit (though deliberately crude) second-moment bound obtained from absolute Fourier summability. The sharper powers of ε used by the paper require the kernel estimates of P-err.

Agreement with the samplewise realization

theorem Anderson4D.ae_measurableMollifiedPotentialL2Op_eq (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : measurableMollifiedPotentialL2Op M ρ lam ε =ᵐ[MeasureTheory.volume] mollifiedPotentialL2Op M ρ lam ε

At positive mollification scale, the measurable multiplication operator agrees almost surely with the original samplewise totalization from L2Realization.

theorem Anderson4D.ae_measurableAndersonK_eq_andersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : measurableAndersonK M ρ lam ε =ᵐ[MeasureTheory.volume] andersonK M ρ lam ε

Consequently the measurable and samplewise realizations of Kε = G Mε agree almost surely.

theorem Anderson4D.ae_norm_sq_measurableAndersonK_eq_andersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : (fun (ω : M.Ω) => ‖measurableAndersonK M ρ lam ε ω‖ ^ 2) =ᵐ[MeasureTheory.volume] fun (ω : M.Ω) => ‖andersonK M ρ lam ε ω‖ ^ 2

Second moment of the random operator

theorem Anderson4D.measurableAndersonK_norm_le_potential (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ‖measurableAndersonK M ρ lam ε ω‖ ≤ ‖measurableMollifiedPotential M ρ lam ε ω‖

theorem Anderson4D.norm_measurableMollifiedPotential_le (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ‖measurableMollifiedPotential M ρ lam ε ω‖ ≤ ‖↑(lamEps lam ε)‖ * ‖xiEpsContinuousMap M ρ ε ω‖ + ‖↑(renormCEps ρ lam ε)‖

theorem Anderson4D.norm_sq_measurableAndersonK_le (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ‖measurableAndersonK M ρ lam ε ω‖ ^ 2 ≤ 2 * ‖↑(lamEps lam ε)‖ ^ 2 * ‖xiEpsContinuousMap M ρ ε ω‖ ^ 2 + 2 * ‖↑(renormCEps ρ lam ε)‖ ^ 2

Pointwise quadratic domination used for both integrability and the Markov bound.

theorem Anderson4D.memLp_measurableMollifiedPotential (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.MemLp (measurableMollifiedPotential M ρ lam ε) 2 MeasureTheory.volume

theorem Anderson4D.integrable_norm_sq_measurableAndersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖measurableAndersonK M ρ lam ε ω‖ ^ 2) MeasureTheory.volume

theorem Anderson4D.integrable_norm_sq_andersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖andersonK M ρ lam ε ω‖ ^ 2) MeasureTheory.volume

theorem Anderson4D.integral_norm_sq_measurableAndersonK_le (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : ∫ (ω : M.Ω), ‖measurableAndersonK M ρ lam ε ω‖ ^ 2 ≤ 2 * ‖↑(lamEps lam ε)‖ ^ 2 * (‖NoiseModel.whiteNoiseFourierScale‖ * ∑' (k : Z4), ‖ρ.symbol ε k‖) ^ 2 + 2 * ‖↑(renormCEps ρ lam ε)‖ ^ 2

theorem Anderson4D.integral_norm_sq_andersonK_le (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : ∫ (ω : M.Ω), ‖andersonK M ρ lam ε ω‖ ^ 2 ≤ 2 * ‖↑(lamEps lam ε)‖ ^ 2 * (‖NoiseModel.whiteNoiseFourierScale‖ * ∑' (k : Z4), ‖ρ.symbol ε k‖) ^ 2 + 2 * ‖↑(renormCEps ρ lam ε)‖ ^ 2

The requested quantitative second moment for the original samplewise operator. All measurability work is discharged by its a.s. agreement with the canonical measurable realization.

theorem Anderson4D.measureReal_compl_andersonResolventGoodEvent_explicit_le (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.volume.real (andersonResolventGoodEvent M ρ lam ε)ᶜ ≤ 4 * (2 * ‖↑(lamEps lam ε)‖ ^ 2 * (‖NoiseModel.whiteNoiseFourierScale‖ * ∑' (k : Z4), ‖ρ.symbol ε k‖) ^ 2 + 2 * ‖↑(renormCEps ρ lam ε)‖ ^ 2)

Markov's inequality with all analytic premises instantiated. This controls the abstract norm-small event, but is not the paper's parametrix good event: the displayed crude bound need not vanish with ε.