One-sided compact-parametrix inversion

The paper estimates the physical identity P L = 1 + R'. After factorizing P = Q G, this is the bounded identity

Q (1 - G M) = 1 + R'.

For an arbitrary bounded operator a small one-sided residual is not enough for invertibility. Here G M is compact, however, so the Fredholm alternative upgrades the resulting injectivity to an honest unit. This avoids imposing an additional residual estimate not present in paper (3.21)--(3.33).

theorem Anderson4D.not_hasEigenvalue_one_of_leftParametrix {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K Q R : H →L[ℂ] H) (hQA : Q * (1 - K) = 1 + R) (hR : ‖R‖ < 1) : ¬Module.End.HasEigenvalue (↑K) 1

A small left parametrix residual excludes eigenvalue 1 for the compact operator K.

theorem Anderson4D.isUnit_one_sub_of_compact_leftParametrix {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K Q R : H →L[ℂ] H) (hcompact : IsCompactOperator ⇑K) (hQA : Q * (1 - K) = 1 + R) (hR : ‖R‖ < 1) : IsUnit (1 - K)

One-sided Fredholm inversion. If K is compact and Q (1-K) differs from the identity by a norm-small residual, then 1-K is a unit.

theorem Anderson4D.inverseUnit_eq_correctedParametrixLeftInverse_of_compact {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K Q R : H →L[ℂ] H) (hcompact : IsCompactOperator ⇑K) (hQA : Q * (1 - K) = 1 + R) (hR : ‖R‖ < 1) : ↑⋯.unit⁻¹ = correctedParametrixLeftInverse Q R hR

The inverse selected by Fredholm is the corrected one-sided parametrix.

theorem Anderson4D.lopInvertible_of_compact_leftParametrix {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G M Q R : H →L[ℂ] H) (hcompact : IsCompactOperator ⇑(Kop G M)) (hleft : Q * (1 - Kop G M) = 1 + R) (hR : ‖R‖ < 1) : LopInvertible G M

Anderson specialization of one-sided Fredholm inversion.

theorem Anderson4D.inverseGreen_eq_correctedLeftParametrix_mul_of_compact {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G M Q R : H →L[ℂ] H) (hcompact : IsCompactOperator ⇑(Kop G M)) (hleft : Q * (1 - Kop G M) = 1 + R) (hR : ‖R‖ < 1) : inverseGreen G M ⋯ = correctedParametrixLeftInverse Q R hR * G

The physical inverse is the corrected left factor followed by G.

theorem Anderson4D.correctedParametrixLeftInverse_mul_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (Q R G : H →L[ℂ] H) (hR : ‖R‖ < 1) : correctedParametrixLeftInverse Q R hR * G - Q * G = (oneAddNeumannInverse R hR - 1) * (Q * G)

Exact factorization of the one-sided correction error.

theorem Anderson4D.norm_inverseGreen_sub_parametrix_mul_le_of_compact {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G M Q R : H →L[ℂ] H) (hcompact : IsCompactOperator ⇑(Kop G M)) (hleft : Q * (1 - Kop G M) = 1 + R) (hR : ‖R‖ < 1) : ‖inverseGreen G M ⋯ - Q * G‖ ≤ (1 - ‖R‖)⁻¹ * ‖R‖ * ‖Q * G‖

Quantitative one-sided error bound in terms of the physical parametrix norm ‖QG‖, exactly the norm controlled in paper (3.31).

theorem Anderson4D.norm_inverseGreen_sub_parametrix_mul_le_two_of_compact {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G M Q R : H →L[ℂ] H) (hcompact : IsCompactOperator ⇑(Kop G M)) (hleft : Q * (1 - Kop G M) = 1 + R) (hRhalf : ‖R‖ < 1 / 2) : ‖inverseGreen G M ⋯ - Q * G‖ ≤ 2 * ‖Q * G‖ * ‖R‖

Half-ball form used by the paper-scale good event.