Two-sided parametrix inversion in the bounded-operator algebra

The paper controls two remainders produced by the left and right parametrix identities. This file isolates the exact Banach-algebra argument those estimates feed:

• if A Q = 1 + Rᵣ and Q A = 1 + Rₗ;
• and both remainder norms are less than one;
• then A is a unit, with inverse Q (1 + Rᵣ)⁻¹ = (1 + Rₗ)⁻¹ Q;
• the inverse differs from Q by at most a geometric remainder.

For the Anderson realization one takes A = 1 - K. The actual kernel-to-operator work in P-err must still construct the bounded operator Q and prove the two displayed identities; no such analytic input is assumed here.

Inverting 1 + R

noncomputable def Anderson4D.oneAddNeumannInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : H →L[ℂ] H) (hR : ‖R‖ < 1) : H →L[ℂ] H

The Neumann inverse of 1 + R, written using the project's canonical inverse of 1 - (-R).

Equations

• Anderson4D.oneAddNeumannInverse R hR = Anderson4D.neumannInverse (-R) ⋯

theorem Anderson4D.one_add_mul_oneAddNeumannInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : H →L[ℂ] H) (hR : ‖R‖ < 1) : (1 + R) * oneAddNeumannInverse R hR = 1

theorem Anderson4D.oneAddNeumannInverse_mul_one_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : H →L[ℂ] H) (hR : ‖R‖ < 1) : oneAddNeumannInverse R hR * (1 + R) = 1

theorem Anderson4D.norm_oneAddNeumannInverse_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (R : H →L[ℂ] H) (hR : ‖R‖ < 1) : ‖oneAddNeumannInverse R hR‖ ≤ (1 - ‖R‖)⁻¹

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

theorem Anderson4D.norm_oneAddNeumannInverse_sub_one_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (R : H →L[ℂ] H) (hR : ‖R‖ < 1) : ‖oneAddNeumannInverse R hR - 1‖ ≤ (1 - ‖R‖)⁻¹ * ‖R‖

Corrected left and right inverses

noncomputable def Anderson4D.correctedParametrixRightInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (Q Rright : H →L[ℂ] H) (hRright : ‖Rright‖ < 1) : H →L[ℂ] H

Right inverse candidate obtained from A Q = 1 + Rᵣ.

Equations

• Anderson4D.correctedParametrixRightInverse Q Rright hRright = Q * Anderson4D.oneAddNeumannInverse Rright hRright

noncomputable def Anderson4D.correctedParametrixLeftInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (Q Rleft : H →L[ℂ] H) (hRleft : ‖Rleft‖ < 1) : H →L[ℂ] H

Left inverse candidate obtained from Q A = 1 + Rₗ.

Equations

• Anderson4D.correctedParametrixLeftInverse Q Rleft hRleft = Anderson4D.oneAddNeumannInverse Rleft hRleft * Q

theorem Anderson4D.correctedParametrixRightInverse_spec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A Q Rright : H →L[ℂ] H) (hAQ : A * Q = 1 + Rright) (hRright : ‖Rright‖ < 1) : A * correctedParametrixRightInverse Q Rright hRright = 1

theorem Anderson4D.correctedParametrixLeftInverse_spec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A Q Rleft : H →L[ℂ] H) (hQA : Q * A = 1 + Rleft) (hRleft : ‖Rleft‖ < 1) : correctedParametrixLeftInverse Q Rleft hRleft * A = 1

theorem Anderson4D.correctedParametrixLeftInverse_eq_rightInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A Q Rleft Rright : H →L[ℂ] H) (hAQ : A * Q = 1 + Rright) (hQA : Q * A = 1 + Rleft) (hRleft : ‖Rleft‖ < 1) (hRright : ‖Rright‖ < 1) : correctedParametrixLeftInverse Q Rleft hRleft = correctedParametrixRightInverse Q Rright hRright

A left and a right inverse of the same operator coincide.

theorem Anderson4D.isUnit_of_twoSidedParametrix {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A Q Rleft Rright : H →L[ℂ] H) (hAQ : A * Q = 1 + Rright) (hQA : Q * A = 1 + Rleft) (hRleft : ‖Rleft‖ < 1) (hRright : ‖Rright‖ < 1) : IsUnit A

The two error identities and norm bounds produce an honest unit.

theorem Anderson4D.inverseUnit_eq_correctedParametrixRightInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A Q Rleft Rright : H →L[ℂ] H) (hAQ : A * Q = 1 + Rright) (hQA : Q * A = 1 + Rleft) (hRleft : ‖Rleft‖ < 1) (hRright : ‖Rright‖ < 1) : ↑⋯.unit⁻¹ = correctedParametrixRightInverse Q Rright hRright

Quantitative error

theorem Anderson4D.correctedParametrixRightInverse_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (Q Rright : H →L[ℂ] H) (hRright : ‖Rright‖ < 1) : correctedParametrixRightInverse Q Rright hRright - Q = Q * (oneAddNeumannInverse Rright hRright - 1)

theorem Anderson4D.norm_correctedParametrixRightInverse_sub_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (Q Rright : H →L[ℂ] H) (hRright : ‖Rright‖ < 1) : ‖correctedParametrixRightInverse Q Rright hRright - Q‖ ≤ ‖Q‖ * ((1 - ‖Rright‖)⁻¹ * ‖Rright‖)

theorem Anderson4D.norm_correctedParametrixRightInverse_sub_le_two {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (Q Rright : H →L[ℂ] H) (hRright : ‖Rright‖ < 1 / 2) : ‖correctedParametrixRightInverse Q Rright ⋯ - Q‖ ≤ 2 * ‖Q‖ * ‖Rright‖

Anderson specialization

structure Anderson4D.AndersonParametrixData {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (G M Q Rleft Rright : H →L[ℂ] H) : Prop

Two-sided parametrix data for the factorized bounded Anderson operator 1 - G M.

• rightIdentity : (1 - Kop G M) * Q = 1 + Rright
• leftIdentity : Q * (1 - Kop G M) = 1 + Rleft

theorem Anderson4D.lopInvertible_of_parametrix_remainders {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G M Q Rleft Rright : H →L[ℂ] H) (hdata : AndersonParametrixData G M Q Rleft Rright) (hRleft : ‖Rleft‖ < 1) (hRright : ‖Rright‖ < 1) : LopInvertible G M

theorem Anderson4D.inverseGreen_eq_correctedParametrix_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G M Q Rleft Rright : H →L[ℂ] H) (hdata : AndersonParametrixData G M Q Rleft Rright) (hRleft : ‖Rleft‖ < 1) (hRright : ‖Rright‖ < 1) : inverseGreen G M ⋯ = correctedParametrixRightInverse Q Rright hRright * G

theorem Anderson4D.norm_inverseGreen_sub_parametrix_mul_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G M Q Rleft Rright : H →L[ℂ] H) (hdata : AndersonParametrixData G M Q Rleft Rright) (hRleft : ‖Rleft‖ < 1) (hRright : ‖Rright‖ < 1) : ‖inverseGreen G M ⋯ - Q * G‖ ≤ ‖Q‖ * ((1 - ‖Rright‖)⁻¹ * ‖Rright‖) * ‖G‖

theorem Anderson4D.norm_inverseGreen_sub_parametrix_mul_le_two {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G M Q Rleft Rright : H →L[ℂ] H) (hdata : AndersonParametrixData G M Q Rleft Rright) (hRleft : ‖Rleft‖ < 1 / 2) (hRright : ‖Rright‖ < 1 / 2) : ‖inverseGreen G M ⋯ - Q * G‖ ≤ 2 * ‖Q‖ * ‖Rright‖ * ‖G‖

Random good event and Chebyshev estimate

def Anderson4D.twoSidedParametrixGoodEvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Ω : Type u_2} (Rleft Rright : Ω → H →L[ℂ] H) : Set Ω

The paper-shaped good event: both left and right remainder norms are smaller than one half.

Equations

• Anderson4D.twoSidedParametrixGoodEvent Rleft Rright = {ω : Ω | ‖Rleft ω‖ < 1 / 2 ∧ ‖Rright ω‖ < 1 / 2}

theorem Anderson4D.compl_twoSidedParametrixGoodEvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Ω : Type u_2} (Rleft Rright : Ω → H →L[ℂ] H) : (twoSidedParametrixGoodEvent Rleft Rright)ᶜ = operatorBadEvent Rleft (1 / 2) ∪ operatorBadEvent Rright (1 / 2)

theorem Anderson4D.measureReal_compl_twoSidedParametrixGoodEvent_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Rleft Rright : Ω → H →L[ℂ] H) (δleft δright : ℝ) (hintLeft : MeasureTheory.Integrable (fun (ω : Ω) => ‖Rleft ω‖ ^ 2) μ) (hintRight : MeasureTheory.Integrable (fun (ω : Ω) => ‖Rright ω‖ ^ 2) μ) (hsecondLeft : ∫ (ω : Ω), ‖Rleft ω‖ ^ 2 ∂μ ≤ δleft) (hsecondRight : ∫ (ω : Ω), ‖Rright ω‖ ^ 2 ∂μ ≤ δright) : μ.real (twoSidedParametrixGoodEvent Rleft Rright)ᶜ ≤ 4 * (δleft + δright)

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

First-moment Markov inequality for an operator norm. This is the form used by paper (3.32), whose hypotheses control 𝔼 (‖R‖ + ‖R'‖) rather than the squares.

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

theorem Anderson4D.measureReal_compl_twoSidedParametrixGoodEvent_le_of_firstMoment {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Rleft Rright : Ω → H →L[ℂ] H) (δleft δright : ℝ) (hintLeft : MeasureTheory.Integrable (fun (ω : Ω) => ‖Rleft ω‖) μ) (hintRight : MeasureTheory.Integrable (fun (ω : Ω) => ‖Rright ω‖) μ) (hfirstLeft : ∫ (ω : Ω), ‖Rleft ω‖ ∂μ ≤ δleft) (hfirstRight : ∫ (ω : Ω), ‖Rright ω‖ ∂μ ≤ δright) : μ.real (twoSidedParametrixGoodEvent Rleft Rright)ᶜ ≤ 2 * (δleft + δright)

Paper-shaped Chebyshev estimate from the expected sum of the two remainder norms.

theorem Anderson4D.lopInvertible_on_twoSidedParametrixGoodEvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {Ω : Type u_2} (G M Q Rleft Rright : Ω → H →L[ℂ] H) (hdata : ∀ (ω : Ω), AndersonParametrixData (G ω) (M ω) (Q ω) (Rleft ω) (Rright ω)) {ω : Ω} (hω : ω ∈ twoSidedParametrixGoodEvent Rleft Rright) : LopInvertible (G ω) (M ω)

theorem Anderson4D.norm_inverseGreen_sub_parametrix_mul_on_goodEvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {Ω : Type u_2} (G M Q Rleft Rright : Ω → H →L[ℂ] H) (hdata : ∀ (ω : Ω), AndersonParametrixData (G ω) (M ω) (Q ω) (Rleft ω) (Rright ω)) {ω : Ω} (hω : ω ∈ twoSidedParametrixGoodEvent Rleft Rright) : ‖inverseGreen (G ω) (M ω) ⋯ - Q ω * G ω‖ ≤ 2 * ‖Q ω‖ * ‖Rright ω‖ * ‖G ω‖