Second-moment good events for bounded random resolvents

This file supplies the probability-theoretic shell of the paper's Chebyshev/Neumann argument. The analytic random-kernel estimate only has to bound E ‖K‖²; Markov's inequality then gives a high-probability half-ball on which the inverse and its deterministic norm bounds exist.

def Anderson4D.operatorBadEvent {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (K : Ω → H →L[ℂ] H) (r : ℝ) : Set Ω

The event that a random bounded operator exceeds a norm threshold.

Equations

• Anderson4D.operatorBadEvent K r = {ω : Ω | r ≤ ‖K ω‖}

theorem Anderson4D.sq_mul_measureReal_operatorBadEvent_le {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : Ω → H →L[ℂ] H) (r : ℝ) (hr : 0 ≤ r) (hint : MeasureTheory.Integrable (fun (ω : Ω) => ‖K ω‖ ^ 2) μ) : r ^ 2 * μ.real (operatorBadEvent K r) ≤ ∫ (ω : Ω), ‖K ω‖ ^ 2 ∂μ

Markov's inequality applied to the squared operator norm.

theorem Anderson4D.measureReal_operatorBadEvent_half_le {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (K : Ω → H →L[ℂ] H) (δ : ℝ) (hint : MeasureTheory.Integrable (fun (ω : Ω) => ‖K ω‖ ^ 2) μ) (hsecond : ∫ (ω : Ω), ‖K ω‖ ^ 2 ∂μ ≤ δ) : μ.real (operatorBadEvent K (1 / 2)) ≤ 4 * δ

At threshold 1/2, a second-moment bound δ gives bad-event probability at most 4δ.

def Anderson4D.resolventGoodEvent {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G : H →L[ℂ] H) (M : Ω → H →L[ℂ] H) : Set Ω

The norm-small event used to construct the random inverse.

Equations

• Anderson4D.resolventGoodEvent G M = {ω : Ω | ‖Anderson4D.Kop G (M ω)‖ < 1 / 2}

theorem Anderson4D.compl_resolventGoodEvent {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G : H →L[ℂ] H) (M : Ω → H →L[ℂ] H) : (resolventGoodEvent G M)ᶜ = operatorBadEvent (fun (ω : Ω) => Kop G (M ω)) (1 / 2)

theorem Anderson4D.lopInvertible_on_resolventGoodEvent {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G : H →L[ℂ] H) (M : Ω → H →L[ℂ] H) {ω : Ω} (hω : ω ∈ resolventGoodEvent G M) : LopInvertible G (M ω)

Every sample in the good event has an inverse.

theorem Anderson4D.norm_inverseGreen_sub_G_on_resolventGoodEvent {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G : H →L[ℂ] H) (M : Ω → H →L[ℂ] H) {ω : Ω} (hω : ω ∈ resolventGoodEvent G M) : ‖inverseGreen G (M ω) ⋯ - G‖ ≤ 2 * (‖G‖ * ‖M ω‖ * ‖G‖)

The recentered inverse obeys the uniform half-ball estimate on the good event.

theorem Anderson4D.measureReal_compl_resolventGoodEvent_le {Ω : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (G : H →L[ℂ] H) (M : Ω → H →L[ℂ] H) (δ : ℝ) (hint : MeasureTheory.Integrable (fun (ω : Ω) => ‖Kop G (M ω)‖ ^ 2) μ) (hsecond : ∫ (ω : Ω), ‖Kop G (M ω)‖ ^ 2 ∂μ ≤ δ) : μ.real (resolventGoodEvent G M)ᶜ ≤ 4 * δ

A second-moment estimate for the random K controls the complement of the resolvent good event.