MIPRE.Background.Repetition.CommutingRepetition.Resolver.Resolvent

Scalar-multiplication monotonicity in the Loewner order #

theorem CommutingRepetition.Resolver.smul_nonneg_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {w : ℝ} (hw : 0 ≤ w) {a : A} (ha : 0 ≤ a) :

0 ≤ w • a

source

theorem CommutingRepetition.Resolver.smul_le_smul_left {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {w : ℝ} (hw : 0 ≤ w) {a b : A} (hab : a ≤ b) :

w • a ≤ w • b

Spectra of positive contractions #

source

theorem CommutingRepetition.Resolver.spectrum_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {x : ℝ} (hx : x ∈ spectrum ℝ F) :

0 ≤ x

source

theorem CommutingRepetition.Resolver.spectrum_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF1 : F ≤ 1) {x : ℝ} (hx : x ∈ spectrum ℝ F) :

x ≤ 1

The resolvent and the resolver fiber #

source

noncomputable def CommutingRepetition.Resolver.res {A : Type u_1} [CStarAlgebra A] (F : A) (u : ℝ) :

The resolvent R_F(u) = (F + u)⁻¹ (eq resolvent-notation).

Equations

CommutingRepetition.Resolver.res F u = cfc (fun (t : ℝ) => (t + u)⁻¹) F

Instances For

source

noncomputable def CommutingRepetition.Resolver.fib {A : Type u_1} [CStarAlgebra A] (F : A) (u : ℝ) :

The resolver fiber f_F(u) = F (F + u)⁻¹ (eq resolver-fiber).

Equations

CommutingRepetition.Resolver.fib F u = cfc (fun (t : ℝ) => t / (t + u)) F

Instances For

source

theorem CommutingRepetition.Resolver.continuousOn_res {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

ContinuousOn (fun (t : ℝ) => (t + u)⁻¹) (spectrum ℝ F)

source

theorem CommutingRepetition.Resolver.continuousOn_fib {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

ContinuousOn (fun (t : ℝ) => t / (t + u)) (spectrum ℝ F)

source

theorem CommutingRepetition.Resolver.continuousOn_add_const {u : ℝ} (s : Set ℝ) :

ContinuousOn (fun (t : ℝ) => t + u) s

source

theorem CommutingRepetition.Resolver.res_isSelfAdjoint {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} :

IsSelfAdjoint (res F u)

source

theorem CommutingRepetition.Resolver.fib_isSelfAdjoint {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} :

IsSelfAdjoint (fib F u)

source

theorem CommutingRepetition.Resolver.res_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

0 ≤ res F u

source

theorem CommutingRepetition.Resolver.fib_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

0 ≤ fib F u

source

theorem CommutingRepetition.Resolver.cfc_add_const_eq {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) :

cfc (fun (t : ℝ) => t + u) F = F + (algebraMap ℝ A) u

cfc (t + u) F = F + u.

source

theorem CommutingRepetition.Resolver.res_mul_add {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

res F u * (F + (algebraMap ℝ A) u) = 1

source

theorem CommutingRepetition.Resolver.add_mul_res {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

(F + (algebraMap ℝ A) u) * res F u = 1

source

theorem CommutingRepetition.Resolver.fib_eq_mul_res {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

fib F u = F * res F u

f_F(u) = F R_F(u).

source

theorem CommutingRepetition.Resolver.fib_eq_res_mul {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

fib F u = res F u * F

f_F(u) = R_F(u) F.

source

theorem CommutingRepetition.Resolver.fib_eq_one_sub {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

fib F u = 1 - u • res F u

f_F(u) = 1 − u R_F(u).

source

theorem CommutingRepetition.Resolver.fib_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

fib F u ≤ 1

source

theorem CommutingRepetition.Resolver.norm_res_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

‖res F u‖ ≤ u⁻¹

source

theorem CommutingRepetition.Resolver.norm_fib_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

‖fib F u‖ ≤ 1

source

theorem CommutingRepetition.Resolver.norm_fib_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

‖fib F u‖ ≤ ‖F‖ / u

source

theorem CommutingRepetition.Resolver.res_mul_res_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} {u : ℝ} (hF0 : 0 ≤ F) (hu : 0 < u) :

res F u * res F u ≤ u⁻¹ • res F u

R_F(u)² ≼ u⁻¹ R_F(u) (the resolvent is bounded by u⁻¹).

The fiber difference identity (node 1.2.6.1) #

source

theorem CommutingRepetition.Resolver.fib_sub_fib {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {u : ℝ} {F G : A} (hF0 : 0 ≤ F) (hG0 : 0 ≤ G) (hu : 0 < u) :

fib F u - fib G u = u • (res F u * (F - G) * res G u)

eq resolver-fiber-difference: f_F(u) − f_G(u) = u R_F(u) (F − G) R_G(u).

source

theorem CommutingRepetition.Resolver.sum_smul_conj {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (X : ι → A) (P Q : A) :

∑ i : ι, w i • (P * X i * Q) = (P * ∑ i : ι, w i • X i) * Q

Pulling scalar weights and a two-sided conjugation out of a finite sum.

source

theorem CommutingRepetition.Resolver.weighted_res_identity {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {u : ℝ} {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (Fs : ι → A) (Fb : A) (hF0 : ∀ (i : ι), 0 ≤ Fs i) (hFb0 : 0 ≤ Fb) (hu : 0 < u) (hmean : ∑ i : ι, w i • Fs i = (∑ i : ι, w i) • Fb) :

∑ i : ι, w i • res (Fs i) u - (∑ i : ι, w i) • res Fb u = (res Fb u * ∑ i : ι, w i • ((Fs i - Fb) * res (Fs i) u * (Fs i - Fb))) * res Fb u

The weighted second-order resolvent identity in the division-free mean form ∑ wₖ Fₖ = W F̄ (eq second-resolvent-rearranged, summed).

The pointwise expectation bound (node 1.2.6.2) #

source

theorem CommutingRepetition.Resolver.pointwise_expectation_bound {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {u : ℝ} {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (Fs : ι → A) (Fb : A) (hF0 : ∀ (i : ι), 0 ≤ Fs i) (hFb0 : 0 ≤ Fb) (hu : 0 < u) (hmean : ∑ i : ι, w i • Fs i = (∑ i : ι, w i) • Fb) :

∑ i : ι, w i • ((fib (Fs i) u - fib Fb u) * (fib (Fs i) u - fib Fb u)) ≤ u • (∑ i : ι, w i • res (Fs i) u - (∑ i : ι, w i) • res Fb u)

eq pointwise-resolver-entropy: for nonnegative weights with ∑ wₖ Fₖ = W F̄, ∑ wₖ (f_{Fₖ}(u) − f_{F̄}(u))² ≼ u (∑ wₖ R_{Fₖ}(u) − W R_{F̄}(u)).