MIPRE.Background.Repetition.CommutingRepetition.Resolver.ResolverKernel

Cutoff sequences #

source

noncomputable def CommutingRepetition.Resolver.αseq (n : ℕ) :

ℝ

Lower cutoff αₙ = 1/(n+1).

Equations

CommutingRepetition.Resolver.αseq n = 1 / (↑n + 1)

Instances For

source

noncomputable def CommutingRepetition.Resolver.Tseq (n : ℕ) :

ℝ

Upper cutoff Tₙ = n + 1.

Equations

CommutingRepetition.Resolver.Tseq n = ↑n + 1

Instances For

source

theorem CommutingRepetition.Resolver.αseq_pos (n : ℕ) :

0 < αseq n

source

theorem CommutingRepetition.Resolver.Tseq_pos (n : ℕ) :

0 < Tseq n

source

theorem CommutingRepetition.Resolver.αseq_le_Tseq (n : ℕ) :

αseq n ≤ Tseq n

source

theorem CommutingRepetition.Resolver.inv_Tseq (n : ℕ) :

(Tseq n)⁻¹ = αseq n

source

theorem CommutingRepetition.Resolver.uIcc_subset_Ioi (n : ℕ) :

Set.uIcc (αseq n) (Tseq n) ⊆ Set.Ioi 0

source

theorem CommutingRepetition.Resolver.tendsto_αseq :

Filter.Tendsto αseq Filter.atTop (nhds 0)

source

theorem CommutingRepetition.Resolver.tendsto_Tseq :

Filter.Tendsto Tseq Filter.atTop Filter.atTop

source

theorem CommutingRepetition.Resolver.tendsto_αseq_add_inv_Tseq :

Filter.Tendsto (fun (n : ℕ) => αseq n + (Tseq n)⁻¹) Filter.atTop (nhds 0)

Improper integrals as cutoff limits #

source

theorem CommutingRepetition.Resolver.tendsto_intervalIntegral_cutoff {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) :

Filter.Tendsto (fun (n : ℕ) => ∫ (u : ℝ) in αseq n..Tseq n, f u) Filter.atTop (nhds (∫ (u : ℝ) in Set.Ioi 0, f u))

For f integrable on (0, ∞), the interval integrals over [αₙ, Tₙ] converge to the integral over (0, ∞).

Positivity of operator-valued integrals #

source

theorem CommutingRepetition.Resolver.convex_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :

Convex ℝ (Set.Ici 0)

source

theorem CommutingRepetition.Resolver.setIntegral_nonneg_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {f : ℝ → A} {s : Set ℝ} (hs : MeasurableSet s) (hfin : MeasureTheory.volume s ≠ ⊤) (hf : MeasureTheory.IntegrableOn f s MeasureTheory.volume) (hpos : ∀ u ∈ s, 0 ≤ f u) :

0 ≤ ∫ (u : ℝ) in s, f u

A set integral of a positive integrand over a set of finite measure is positive.

source

theorem CommutingRepetition.Resolver.intervalIntegral_nonneg_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {f : ℝ → A} {a b : ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f MeasureTheory.volume a b) (hpos : ∀ u ∈ Set.Ioc a b, 0 ≤ f u) :

0 ≤ ∫ (u : ℝ) in a..b, f u

source

theorem CommutingRepetition.Resolver.intervalIntegral_mono_of_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {f g : ℝ → A} {a b : ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) (h : ∀ u ∈ Set.Ioc a b, f u ≤ g u) :

∫ (u : ℝ) in a..b, f u ≤ ∫ (u : ℝ) in a..b, g u

The Gram kernel #

source

noncomputable def CommutingRepetition.Resolver.kern {A : Type u_1} [CStarAlgebra A] (F G : A) :

The resolver Gram kernel ∫₀^∞ F(F+u)⁻¹ G(G+u)⁻¹ du.

Equations

CommutingRepetition.Resolver.kern F G = ∫ (u : ℝ) in Set.Ioi 0, CommutingRepetition.Resolver.fib F u * CommutingRepetition.Resolver.fib G u

Instances For

source

theorem CommutingRepetition.Resolver.continuousOn_fib_mul_fib {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F G : A} (hF0 : 0 ≤ F) (hG0 : 0 ≤ G) :

ContinuousOn (fun (u : ℝ) => fib F u * fib G u) (Set.Ioi 0)

source

theorem CommutingRepetition.Resolver.intervalIntegrable_fib_mul_fib {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F G : A} (hF0 : 0 ≤ F) (hG0 : 0 ≤ G) (n : ℕ) :

IntervalIntegrable (fun (u : ℝ) => fib F u * fib G u) MeasureTheory.volume (αseq n) (Tseq n)

source

theorem CommutingRepetition.Resolver.integrableOn_fib_mul_fib {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F G : A} (hF0 : 0 ≤ F) (hG0 : 0 ≤ G) :

MeasureTheory.IntegrableOn (fun (u : ℝ) => fib F u * fib G u) (Set.Ioi 0) MeasureTheory.volume

Integrability of the kernel integrand on (0, ∞): bounded by 1 near 0 and by ‖F‖ ‖G‖ / u² at infinity.

source

theorem CommutingRepetition.Resolver.tendsto_intervalIntegral_kern {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F G : A} (hF0 : 0 ≤ F) (hG0 : 0 ≤ G) :

Filter.Tendsto (fun (n : ℕ) => ∫ (u : ℝ) in αseq n..Tseq n, fib F u * fib G u) Filter.atTop (nhds (kern F G))

The cutoff integrals converge to the kernel.

source

theorem CommutingRepetition.Resolver.kern_self {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) (hF1 : F ≤ 1) :

kern F F = F

K(F, F) = F.

source

theorem CommutingRepetition.Resolver.kern_star {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (F G : A) :

star (kern F G) = kern G F

K(F, G)* = K(G, F).

The kernel entropy inequality #

source

theorem CommutingRepetition.Resolver.tendsto_Ecorr {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) (hF1 : F ≤ 1) :

Filter.Tendsto (fun (n : ℕ) => Ecorr (αseq n) (Tseq n) F) Filter.atTop (nhds (-cfc Real.negMulLog F))

The entropic correction converges to −negMulLog(F) along the cutoffs.

source

theorem CommutingRepetition.Resolver.continuousOn_diffsq {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (Fs : ι → A) (Fb : A) (hF0 : ∀ (i : ι), 0 ≤ Fs i) (hFb0 : 0 ≤ Fb) (n : ℕ) :

ContinuousOn (fun (u : ℝ) => ∑ i : ι, w i • ((fib (Fs i) u - fib Fb u) * (fib (Fs i) u - fib Fb u))) (Set.uIcc (αseq n) (Tseq n))

Continuity on [αₙ, Tₙ] of the weighted difference-square integrand.

source

theorem CommutingRepetition.Resolver.continuousOn_wres {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (Fs : ι → A) (Fb : A) (hF0 : ∀ (i : ι), 0 ≤ Fs i) (hFb0 : 0 ≤ Fb) (n : ℕ) :

ContinuousOn (fun (u : ℝ) => u • (∑ i : ι, w i • res (Fs i) u - (∑ i : ι, w i) • res Fb u)) (Set.uIcc (αseq n) (Tseq n))

Continuity on [αₙ, Tₙ] of the weighted resolvent integrand.

source

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

∫ (u : ℝ) in αseq n..Tseq n, ∑ i : ι, w i • ((fib (Fs i) u - fib Fb u) * (fib (Fs i) u - fib Fb u)) ≤ ∫ (u : ℝ) in αseq n..Tseq n, u • (∑ i : ι, w i • res (Fs i) u - (∑ i : ι, w i) • res Fb u)

The integrated pointwise bound (node 1.2.6.2 over [αₙ, Tₙ]).

source

theorem CommutingRepetition.Resolver.integral_wres {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (Fs : ι → A) (Fb : A) (hF0 : ∀ (i : ι), 0 ≤ Fs i) (hFb0 : 0 ≤ Fb) (n : ℕ) :

∫ (u : ℝ) in αseq n..Tseq n, u • (∑ i : ι, w i • res (Fs i) u - (∑ i : ι, w i) • res Fb u) = ∑ i : ι, w i • cfc (hfun (αseq n) (Tseq n)) (Fs i) - (∑ i : ι, w i) • cfc (hfun (αseq n) (Tseq n)) Fb

Evaluation of the right side: ∑ wᵢ hfun(Fᵢ) − W hfun(F̄).

source

theorem CommutingRepetition.Resolver.integral_diffsq {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (Fs : ι → A) (Fb : A) (hF0 : ∀ (i : ι), 0 ≤ Fs i) (hFb0 : 0 ≤ Fb) (n : ℕ) :

∫ (u : ℝ) in αseq n..Tseq n, ∑ i : ι, w i • ((fib (Fs i) u - fib Fb u) * (fib (Fs i) u - fib Fb u)) = ∑ i : ι, w i • ((((∫ (u : ℝ) in αseq n..Tseq n, fib (Fs i) u * fib (Fs i) u) - ∫ (u : ℝ) in αseq n..Tseq n, fib (Fs i) u * fib Fb u) - ∫ (u : ℝ) in αseq n..Tseq n, fib Fb u * fib (Fs i) u) + ∫ (u : ℝ) in αseq n..Tseq n, fib Fb u * fib Fb u)

Evaluation of the left side as a combination of cutoff kernel integrals.

source

theorem CommutingRepetition.Resolver.wsum_cancel {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {ι : Type u_2} [Fintype ι] (w : ι → ℝ) (Fs : ι → A) (Fb : A) (hmean : ∑ i : ι, w i • Fs i = (∑ i : ι, w i) • Fb) (c : A) (r : ℝ) (E : ι → A) (Eb : A) :

∑ i : ι, w i • (c - r • Fs i + E i) - (∑ i : ι, w i) • (c - r • Fb + Eb) = ∑ i : ι, w i • E i - (∑ i : ι, w i) • Eb

Algebra of the right side: the constant and linear parts cancel by ∑ wᵢ Fᵢ = W F̄.

source

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

∑ i : ι, w i • (kern (Fs i) (Fs i) - kern (Fs i) Fb - kern Fb (Fs i) + kern Fb Fb) ≤ (∑ i : ι, w i) • cfc Real.negMulLog Fb - ∑ i : ι, w i • cfc Real.negMulLog (Fs i)

Kernel entropy inequality.

Membership of the kernel in closed star subalgebras #

source

theorem CommutingRepetition.Resolver.setIntegral_mem_of_closed {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {C : Set A} (hconv : Convex ℝ C) (hcl : IsClosed C) (h0 : 0 ∈ C) (hscale : ∀ (r : ℝ), 0 ≤ r → ∀ x ∈ C, r • x ∈ C) {f : ℝ → A} {s : Set ℝ} (hs : MeasurableSet s) (hfin : MeasureTheory.volume s ≠ ⊤) (hf : MeasureTheory.IntegrableOn f s MeasureTheory.volume) (hmem : ∀ u ∈ s, f u ∈ C) :

∫ (u : ℝ) in s, f u ∈ C

source

theorem CommutingRepetition.Resolver.intervalIntegral_mem_of_closed {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {C : Set A} (hconv : Convex ℝ C) (hcl : IsClosed C) (h0 : 0 ∈ C) (hscale : ∀ (r : ℝ), 0 ≤ r → ∀ x ∈ C, r • x ∈ C) {f : ℝ → A} {a b : ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmem : ∀ u ∈ Set.Ioc a b, f u ∈ C) :

∫ (u : ℝ) in a..b, f u ∈ C

source

theorem CommutingRepetition.Resolver.real_smul_mem {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (S : StarSubalgebra ℂ A) (r : ℝ) {x : A} (hx : x ∈ S) :

r • x ∈ S

source

theorem CommutingRepetition.Resolver.convex_starSubalgebra {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (S : StarSubalgebra ℂ A) :

Convex ℝ ↑S

source

theorem CommutingRepetition.Resolver.fib_mem {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {S : StarSubalgebra ℂ A} (hS : IsClosed ↑S) {F : A} (hF : F ∈ S) (u : ℝ) :

fib F u ∈ S

source

theorem CommutingRepetition.Resolver.res_mem {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {S : StarSubalgebra ℂ A} (hS : IsClosed ↑S) {F : A} (hF : F ∈ S) (u : ℝ) :

res F u ∈ S

source

theorem CommutingRepetition.Resolver.kern_mem {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {S : StarSubalgebra ℂ A} (hS : IsClosed ↑S) {F G : A} (hF0 : 0 ≤ F) (hG0 : 0 ≤ G) (hF : F ∈ S) (hG : G ∈ S) :

kern F G ∈ S

The kernel of two elements of a closed star subalgebra lies in it.