The exchange theorem

theorem CommutingRepetition.Resolver.continuousOn_cfc_param {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {C : A} (hC : IsSelfAdjoint C) (g : ℝ → ℝ → ℝ) {s : Set ℝ} (hg : ContinuousOn (Function.uncurry g) (s ×ˢ spectrum ℝ C)) : ContinuousOn (fun (u : ℝ) => cfc (g u) C) s

Parametrized cfc is continuous in the parameter wherever the two-variable function is jointly continuous on s × spectrum.

theorem CommutingRepetition.Resolver.intervalIntegral_cfc {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {C : A} (hC : IsSelfAdjoint C) (g : ℝ → ℝ → ℝ) {α T : ℝ} (hg : ContinuousOn (Function.uncurry g) (Set.uIcc α T ×ˢ spectrum ℝ C)) : ∫ (u : ℝ) in α..T, cfc (g u) C = cfc (fun (t : ℝ) => ∫ (u : ℝ) in α..T, g u t) C

Integral/CFC exchange.

Scalar integrals (fundamental theorem of calculus)

theorem CommutingRepetition.Resolver.add_pos_of_mem_uIcc {t α T u : ℝ} (ht : 0 ≤ t) (hα : 0 < α) (hT : 0 < T) (hu : u ∈ Set.uIcc α T) : 0 < t + u

Positivity of t + u on the relevant set.

theorem CommutingRepetition.Resolver.integral_smul_res_scalar {t α T : ℝ} (ht : 0 ≤ t) (hα : 0 < α) (hT : 0 < T) : ∫ (u : ℝ) in α..T, u * (t + u)⁻¹ = T - α - t * Real.log (t + T) + t * Real.log (t + α)

∫ₐᵀ u/(t+u) du = (T − α) − t log(t+T) + t log(t+α).

theorem CommutingRepetition.Resolver.integral_fib_sq_scalar {t α T : ℝ} (ht : 0 ≤ t) (hα : 0 < α) (hT : 0 < T) : ∫ (u : ℝ) in α..T, t / (t + u) * (t / (t + u)) = t ^ 2 * ((t + α)⁻¹ - (t + T)⁻¹)

∫ₐᵀ (t/(t+u))² du = t² ((t+α)⁻¹ − (t+T)⁻¹).

Operator integrals of the resolvent family

noncomputable def CommutingRepetition.Resolver.hfun (α T t : ℝ) : ℝ

The antiderivative of u ↦ u/(t+u): (T − α) − t log(t+T) + t log(t+α).

Equations

• CommutingRepetition.Resolver.hfun α T t = T - α - t * Real.log (t + T) + t * Real.log (t + α)

noncomputable def CommutingRepetition.Resolver.gfun (α T t : ℝ) : ℝ

The antiderivative of u ↦ (t/(t+u))²: t² ((t+α)⁻¹ − (t+T)⁻¹).

Equations

• CommutingRepetition.Resolver.gfun α T t = t ^ 2 * ((t + α)⁻¹ - (t + T)⁻¹)

theorem CommutingRepetition.Resolver.continuousOn_uncurry_res {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {α T : ℝ} (hα : 0 < α) (hT : 0 < T) : ContinuousOn (Function.uncurry fun (u t : ℝ) => u * (t + u)⁻¹) (Set.uIcc α T ×ˢ spectrum ℝ F)

Joint continuity of (u, t) ↦ u/(t+u) on [α, T] × spectrum.

theorem CommutingRepetition.Resolver.continuousOn_uncurry_fib {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {α T : ℝ} (hα : 0 < α) (hT : 0 < T) : ContinuousOn (Function.uncurry fun (u t : ℝ) => t / (t + u)) (Set.uIcc α T ×ˢ spectrum ℝ F)

Joint continuity of (u, t) ↦ t/(t+u) on [α, T] × spectrum.

theorem CommutingRepetition.Resolver.integral_smul_res {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {α T : ℝ} (hα : 0 < α) (hT : 0 < T) : ∫ (u : ℝ) in α..T, u • res F u = cfc (hfun α T) F

∫ₐᵀ u • res F u du = hfun α T (F).

theorem CommutingRepetition.Resolver.integral_fib_mul_fib {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {α T : ℝ} (hα : 0 < α) (hT : 0 < T) : ∫ (u : ℝ) in α..T, fib F u * fib F u = cfc (gfun α T) F

∫ₐᵀ fib F u * fib F u du = gfun α T (F).

theorem CommutingRepetition.Resolver.continuousOn_res_param {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) : ContinuousOn (fun (u : ℝ) => res F u) (Set.Ioi 0)

Continuity of u ↦ res F u on (0, ∞).

theorem CommutingRepetition.Resolver.continuousOn_fib_param {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) : ContinuousOn (fun (u : ℝ) => fib F u) (Set.Ioi 0)

Continuity of u ↦ fib F u on (0, ∞).

The two-cutoff limits as norm bounds

theorem CommutingRepetition.Resolver.abs_gfun_sub_le {t α T : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hα : 0 < α) (hT : 0 < T) : |gfun α T t - t| ≤ α + T⁻¹

Scalar bound: |gfun α T t − t| ≤ α + T⁻¹ on [0, 1].

theorem CommutingRepetition.Resolver.norm_cfc_gfun_sub_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) (hF1 : F ≤ 1) {α T : ℝ} (hα : 0 < α) (hT : 0 < T) : ‖cfc (gfun α T) F - F‖ ≤ α + T⁻¹

‖gfun α T (F) − F‖ ≤ α + T⁻¹ for a positive contraction F.

noncomputable def CommutingRepetition.Resolver.Ecorr {A : Type u_1} [CStarAlgebra A] (α T : ℝ) (F : A) : A

The entropic correction: t log(t+α) − t log(1 + t/T) applied to F.

Equations

• CommutingRepetition.Resolver.Ecorr α T F = cfc (fun (t : ℝ) => t * Real.log (t + α)) F - cfc (fun (t : ℝ) => t * Real.log (1 + t / T)) F

theorem CommutingRepetition.Resolver.continuousOn_mul_log_add {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {α : ℝ} (hα : 0 < α) : ContinuousOn (fun (t : ℝ) => t * Real.log (t + α)) (spectrum ℝ F)

theorem CommutingRepetition.Resolver.continuousOn_mul_log_one_add_div {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {T : ℝ} (hT : 0 < T) : ContinuousOn (fun (t : ℝ) => t * Real.log (1 + t / T)) (spectrum ℝ F)

theorem CommutingRepetition.Resolver.cfc_hfun_eq {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {α T : ℝ} (hα : 0 < α) (hT : 0 < T) : cfc (hfun α T) F = (T - α) • 1 - Real.log T • F + Ecorr α T F

Decomposition of hfun α T (F) into its constant, linear and correction parts.

theorem CommutingRepetition.Resolver.abs_ecorr_scalar_le {t α T : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hα : 0 < α) (hT : 0 < T) : |t * Real.log (t + α) - t * Real.log (1 + t / T) + t.negMulLog| ≤ α + T⁻¹

Scalar bound for the entropic correction on [0, 1]: |t log(t+α) − t log(1+t/T) + negMulLog t| ≤ α + T⁻¹.

theorem CommutingRepetition.Resolver.norm_Ecorr_add_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) (hF1 : F ≤ 1) {α T : ℝ} (hα : 0 < α) (hT : 0 < T) : ‖Ecorr α T F + cfc Real.negMulLog F‖ ≤ α + T⁻¹

‖Ecorr α T F + cfc negMulLog F‖ ≤ α + T⁻¹ for a positive contraction F.