Quantitative bounds for the bounded resolvent realization

This is the abstract Banach-algebra part of blueprint node I-l2op. It turns the norm-small event for K = G M into explicit Neumann inverse, tail, and recentered-resolvent bounds. No random-kernel estimate enters here; those estimates only have to prove that the event occurs with high probability.

theorem Anderson4D.norm_neumannInverse_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (K : H →L[ℂ] H) (hK : ‖K‖ < 1) : ‖neumannInverse K hK‖ ≤ (1 - ‖K‖)⁻¹

The geometric-series bound for the canonical Neumann inverse.

theorem Anderson4D.norm_neumannInverse_le_two {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (K : H →L[ℂ] H) (hKhalf : ‖K‖ ≤ 1 / 2) : ‖neumannInverse K ⋯‖ ≤ 2

On the paper's convenient half-ball, the inverse has norm at most two.

theorem Anderson4D.neumannInverse_sub_partialSum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : H →L[ℂ] H) (hK : ‖K‖ < 1) (n : ℕ) : neumannInverse K hK - ∑ i ∈ Finset.range n, K ^ i = K ^ n * neumannInverse K hK

Exact algebraic remainder after truncating the Neumann series at order n - 1.

theorem Anderson4D.norm_neumannInverse_sub_partialSum_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (K : H →L[ℂ] H) (hK : ‖K‖ < 1) (n : ℕ) : ‖neumannInverse K hK - ∑ i ∈ Finset.range n, K ^ i‖ ≤ ‖K‖ ^ n * (1 - ‖K‖)⁻¹

Quantitative geometric tail bound.

theorem Anderson4D.norm_inverseGreen_sub_G_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G M : H →L[ℂ] H) (hK : ‖Kop G M‖ < 1) : ‖inverseGreen G M ⋯ - G‖ ≤ (1 - ‖Kop G M‖)⁻¹ * (‖G‖ * ‖M‖ * ‖G‖)

Abstract recentered-resolvent bound on the norm-small event.

theorem Anderson4D.norm_inverseGreen_sub_G_le_two {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G M : H →L[ℂ] H) (hKhalf : ‖Kop G M‖ ≤ 1 / 2) : ‖inverseGreen G M ⋯ - G‖ ≤ 2 * (‖G‖ * ‖M‖ * ‖G‖)

Half-ball specialization used by good-event estimates.