Bounded-operator realization of the resolvent

This file contains only bounded operators and therefore avoids representing 1 - Δ, point masses, or multiplication by a distribution as unbounded operators.

For bounded G and M, set K = G M. Invertibility of the Anderson operator is represented by invertibility of 1 - K. On that event the recentered resolvent satisfies

(1 - K)⁻¹ G - G = (1 - K)⁻¹ G M G.

The norm-small case is connected to the actual Neumann series in the complete operator algebra.

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

The bounded operator K = G ∘ M.

Equations

• Anderson4D.Kop G M = G * M

def Anderson4D.LopInvertible {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G M : H →L[ℂ] H) : Prop

The project definition of invertibility of the corresponding Anderson operator: 1 - K is a unit of the bounded-operator algebra.

Equations

• Anderson4D.LopInvertible G M = IsUnit (1 - Anderson4D.Kop G M)

noncomputable def Anderson4D.inverseGreen {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G M : H →L[ℂ] H) (h : LopInvertible G M) : H →L[ℂ] H

The inverse Green operator on the invertibility event.

Equations

• Anderson4D.inverseGreen G M h = ↑(IsUnit.unit h)⁻¹ * G

noncomputable def Anderson4D.operatorModeCoeffH {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G M : H →L[ℂ] H) (e : Z4 → H) (α β : Z4) : ℂ

Matrix coefficient of the recentered inverse with the sign convention of paper (3.23), junk-totalized to zero off the invertibility event.

Equations

• Anderson4D.operatorModeCoeffH G M e α β = if h : Anderson4D.LopInvertible G M then inner ℂ (e (-α)) ((Anderson4D.inverseGreen G M h) (e β) - G (e β)) else 0

theorem Anderson4D.inverseUnit_mul_one_sub_Kop {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G M : H →L[ℂ] H) (h : LopInvertible G M) : ↑(IsUnit.unit h)⁻¹ * (1 - Kop G M) = 1

The inverse unit is a two-sided inverse of 1 - K.

theorem Anderson4D.inverseGreen_sub_G {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G M : H →L[ℂ] H) (h : LopInvertible G M) : inverseGreen G M h - G = ↑(IsUnit.unit h)⁻¹ * (G * M * G)

Algebraic core of the conditioned Hilbert--Schmidt difference argument.

theorem Anderson4D.inverseGreen_apply_sub_G {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G M : H →L[ℂ] H) (h : LopInvertible G M) (f : H) : (inverseGreen G M h) f - G f = ↑(IsUnit.unit h)⁻¹ (G (M (G f)))

Pointwise form of inverseGreen_sub_G.

theorem Anderson4D.lopInvertible_of_norm_Kop_lt_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G M : H →L[ℂ] H) (hK : ‖Kop G M‖ < 1) : LopInvertible G M

A norm-small K gives the required invertibility event.

noncomputable def Anderson4D.neumannInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : H →L[ℂ] H) (hK : ‖K‖ < 1) : H →L[ℂ] H

The canonical Neumann inverse of 1 - K when ‖K‖ < 1.

Equations

• Anderson4D.neumannInverse K hK = ↑(Units.oneSub K hK)⁻¹

theorem Anderson4D.neumannInverse_eq_tsum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : H →L[ℂ] H) (hK : ‖K‖ < 1) : neumannInverse K hK = ∑' (n : ℕ), K ^ n

The Neumann inverse is the sum of the operator-valued geometric series.

theorem Anderson4D.summable_pow_of_norm_lt_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : H →L[ℂ] H) (hK : ‖K‖ < 1) : Summable fun (n : ℕ) => K ^ n

The operator-valued Neumann series is summable.

theorem Anderson4D.neumannInverse_apply_eq_tsum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : H →L[ℂ] H) (hK : ‖K‖ < 1) (f : H) : (neumannInverse K hK) f = ∑' (n : ℕ), (K ^ n) f

Applying the Neumann inverse agrees with the pointwise sum of the iterated operators.

theorem Anderson4D.inverseGreen_of_norm_lt_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G M : H →L[ℂ] H) (hK : ‖Kop G M‖ < 1) : inverseGreen G M ⋯ = neumannInverse (Kop G M) hK * G

The canonical inverse used by the norm-small event is exactly the inverse selected by its IsUnit witness.