Documentation

MIPRE.Background.Repetition.CommutingRepetition.VN.Modular.CentralExp

J · J as a real star-algebra homomorphism #

source
theorem CommutingRepetition.VN.Modular.conjJm_real_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (c : ℝ) (G : K →L[ℂ] K) :
conjJm M Ω (c • G) = c • conjJm M Ω G
source
theorem CommutingRepetition.VN.Modular.conjJm_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) :
IsSelfAdjoint (conjJm M Ω E)
source
noncomputable def CommutingRepetition.VN.Modular.conjJmHom {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) :
(K →L[ℂ] K) →⋆ₐ[ℝ] K →L[ℂ] K

G ↦ J G J as a unital real star-algebra homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CommutingRepetition.VN.Modular.conjJmHom_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (G : K →L[ℂ] K) :
    (conjJmHom M Ω hs hc) G = conjJm M Ω G
    source
    theorem CommutingRepetition.VN.Modular.continuous_conjJmHom {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) :
    Continuous ⇑(conjJmHom M Ω hs hc)
    source
    theorem CommutingRepetition.VN.Modular.conjJm_cfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {f : ℝ → ℝ} (hf : Continuous f) :
    conjJm M Ω (cfc f E) = cfc f (conjJm M Ω E)

    J f(E) J = f(J E J) for continuous real f.

    source
    theorem CommutingRepetition.VN.Modular.conjJm_commute {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {G H : K →L[ℂ] K} (h : Commute G H) :
    Commute (conjJm M Ω G) (conjJm M Ω H)
    source
    theorem CommutingRepetition.VN.Modular.conjJm_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) :
    conjJm M Ω (R M Ω) = 2 - R M Ω
    source
    theorem CommutingRepetition.VN.Modular.commute_conjJm_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (h : Commute a (R M Ω)) :
    Commute (conjJm M Ω a) (R M Ω)

    J a J commutes with R when a does.

    source
    theorem CommutingRepetition.VN.Modular.Jm_conjJm_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (G : K →L[ℂ] K) (ξ : K) :
    (Jm M Ω) ((conjJm M Ω G) ξ) = G ((Jm M Ω) ξ)

    Exponentials of a self-adjoint operator #

    source
    noncomputable def CommutingRepetition.VN.Modular.expA {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (E : K →L[ℂ] K) (r : ℝ) :
    K →L[ℂ] K

    e^{r E} for a self-adjoint E.

    Equations
    Instances For
      source
      theorem CommutingRepetition.VN.Modular.expA_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (r : ℝ) :
      IsSelfAdjoint (expA E r)
      source
      theorem CommutingRepetition.VN.Modular.expA_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (r s : ℝ) :
      expA E r * expA E s = expA E (r + s)
      source
      theorem CommutingRepetition.VN.Modular.expA_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) :
      expA E 0 = 1
      source
      theorem CommutingRepetition.VN.Modular.expA_mul_neg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (r : ℝ) :
      expA E r * expA E (-r) = 1
      source
      theorem CommutingRepetition.VN.Modular.expA_neg_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (r : ℝ) :
      expA E (-r) * expA E r = 1
      source
      theorem CommutingRepetition.VN.Modular.expA_comm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (r s : ℝ) :
      expA E r * expA E s = expA E s * expA E r
      source
      theorem CommutingRepetition.VN.Modular.expA_apply_expA_neg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (r : ℝ) (ξ : K) :
      (expA E r) ((expA E (-r)) ξ) = ξ
      source
      theorem CommutingRepetition.VN.Modular.expA_neg_apply_expA {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (r : ℝ) (ξ : K) :
      (expA E (-r)) ((expA E r) ξ) = ξ
      source
      theorem CommutingRepetition.VN.Modular.expA_real_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (E : K →L[ℂ] K) (r c : ℝ) (x : K) :
      (expA E r) (c • x) = c • (expA E r) x
      source
      theorem CommutingRepetition.VN.Modular.expA_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (N : VonNeumannAlgebra K) (hEN : E ∈ N) (r : ℝ) :
      expA E r ∈ N
      source
      theorem CommutingRepetition.VN.Modular.commute_expA {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E T : K →L[ℂ] K} (h : Commute E T) (r : ℝ) :
      Commute (expA E r) T

      The reflected element a' = J a J #

      source
      theorem CommutingRepetition.VN.Modular.conjJm_expA {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (hsa : IsSelfAdjoint a) (r : ℝ) :
      conjJm M Ω (expA a r) = expA (conjJm M Ω a) r
      source
      theorem CommutingRepetition.VN.Modular.Jm_expA_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (hsa : IsSelfAdjoint a) (r : ℝ) (ξ : K) :
      (Jm M Ω) ((expA (conjJm M Ω a) r) ξ) = (expA a r) ((Jm M Ω) ξ)
      source
      theorem CommutingRepetition.VN.Modular.expA_conjJm_mem_commutant {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (r : ℝ) :
      expA (conjJm M Ω a) r ∈ M.commutant
      source
      theorem CommutingRepetition.VN.Modular.commute_expA_expA_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (r s : ℝ) :
      Commute (expA a r) (expA (conjJm M Ω a) s)
      source
      theorem CommutingRepetition.VN.Modular.commute_expA_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a : K →L[ℂ] K} (haR : Commute a (R M Ω)) (r : ℝ) :
      Commute (expA a r) (R M Ω)
      source
      theorem CommutingRepetition.VN.Modular.commute_expA_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a : K →L[ℂ] K} (haR : Commute a (R M Ω)) (r : ℝ) :
      Commute (expA a r) (Tm M Ω)
      source
      theorem CommutingRepetition.VN.Modular.commute_expA_conjJm_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (haR : Commute a (R M Ω)) (r : ℝ) :
      Commute (expA (conjJm M Ω a) r) (R M Ω)
      source
      theorem CommutingRepetition.VN.Modular.commute_expA_conjJm_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (haR : Commute a (R M Ω)) (r : ℝ) :
      Commute (expA (conjJm M Ω a) r) (Tm M Ω)

      The perturbed vector ξ = e^{-a/2} Ω #

      source
      theorem CommutingRepetition.VN.Modular.Jm_eq_self_of_R_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {k : K} (hk : k ∈ Kre M Ω) (hR : (R M Ω) k = k) :
      (Jm M Ω) k = k

      On 𝒦, R k = k forces J k = k.

      source
      noncomputable def CommutingRepetition.VN.Modular.pvec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) (a : K →L[ℂ] K) :
      K

      The perturbed vector e^{-a/2} Ω.

      Equations
      Instances For
        source
        theorem CommutingRepetition.VN.Modular.expA_Ω_eq_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) (r : ℝ) :
        (expA (conjJm M Ω a) r) Ω = (expA a r) Ω
        source
        theorem CommutingRepetition.VN.Modular.pvec_eq_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :
        (expA (conjJm M Ω a) (-(1 / 2))) Ω = pvec Ω a
        source
        theorem CommutingRepetition.VN.Modular.isCyclic_pvec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) :
        IsCyclic (↑M) (pvec Ω a)
        source
        theorem CommutingRepetition.VN.Modular.isSeparating_pvec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) :
        IsSeparating (↑M) (pvec Ω a)

        Transport of the standard subspace: 𝒦(M, ξ) = e^{-a'/2} 𝒦(M, Ω) #

        source
        theorem CommutingRepetition.VN.Modular.expA_conjJm_mem_Kre_pvec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) {k : K} (hk : k ∈ Kre M Ω) :
        (expA (conjJm M Ω a) (-(1 / 2))) k ∈ Kre M (pvec Ω a)

        e^{-a'/2} 𝒦(M, Ω) ⊆ 𝒦(M, ξ).

        source
        theorem CommutingRepetition.VN.Modular.expA_conjJm_mem_Kre_of_mem_Kre_pvec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) {η : K} (hη : η ∈ Kre M (pvec Ω a)) :
        (expA (conjJm M Ω a) (1 / 2)) η ∈ Kre M Ω

        e^{a'/2} 𝒦(M, ξ) ⊆ 𝒦(M, Ω).

        source
        theorem CommutingRepetition.VN.Modular.expA_conjJm_mem_orthogonal {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) {η : K} (hη : η ∈ (↑(Kre M (pvec Ω a)))ᗮ) :
        (expA (conjJm M Ω a) (-(1 / 2))) η ∈ (↑(Kre M Ω))ᗮ

        e^{-a'/2} 𝒦(M, ξ)ᗮ ⊆ 𝒦(M, Ω)ᗮ.

        Unitary groups and the factorization e^{it(b-a)} = e^{itb} e^{-ita} #

        source
        noncomputable def CommutingRepetition.VN.Modular.eitf (t l : ℝ) :
        ℂ

        The function l ↦ e^{itl}.

        Equations
        Instances For
          source
          theorem CommutingRepetition.VN.Modular.norm_eitf (t l : ℝ) :
          ‖eitf t l‖ = 1
          source
          theorem CommutingRepetition.VN.Modular.continuous_eitf (t : ℝ) :
          Continuous (eitf t)
          source
          theorem CommutingRepetition.VN.Modular.cbdd_eitf (t : ℝ) :
          BorelCalc.CBdd (eitf t)
          source
          theorem CommutingRepetition.VN.Modular.eitf_add (s t l : ℝ) :
          eitf (s + t) l = eitf s l * eitf t l
          source
          theorem CommutingRepetition.VN.Modular.eitf_zero (l : ℝ) :
          eitf 0 l = 1
          source
          theorem CommutingRepetition.VN.Modular.eitf_sub_arg (t u v : ℝ) :
          eitf t (v - u) = eitf t v * eitf (-t) u
          source
          noncomputable def CommutingRepetition.VN.Modular.eit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (E : K →L[ℂ] K) (hE : IsSelfAdjoint E) (t : ℝ) :
          K →L[ℂ] K

          The unitary group e^{itE}.

          Equations
          Instances For
            source
            theorem CommutingRepetition.VN.Modular.eit_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (s t : ℝ) :
            eit E hE (s + t) = eit E hE s * eit E hE t
            source
            theorem CommutingRepetition.VN.Modular.eit_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) :
            eit E hE 0 = 1
            source
            theorem CommutingRepetition.VN.Modular.eit_mul_neg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (t : ℝ) :
            eit E hE t * eit E hE (-t) = 1
            source
            theorem CommutingRepetition.VN.Modular.eit_neg_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (t : ℝ) :
            eit E hE (-t) * eit E hE t = 1
            source
            theorem CommutingRepetition.VN.Modular.eit_comm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (s t : ℝ) :
            eit E hE s * eit E hE t = eit E hE t * eit E hE s
            source
            theorem CommutingRepetition.VN.Modular.eit_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (t : ℝ) :
            star (eit E hE t) = eit E hE (-t)
            source
            theorem CommutingRepetition.VN.Modular.eit_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (N : VonNeumannAlgebra K) (hEN : E ∈ N) (t : ℝ) :
            eit E hE t ∈ N
            source
            theorem CommutingRepetition.VN.Modular.commute_eit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {T : K →L[ℂ] K} (h : Commute E T) (t : ℝ) :
            Commute (eit E hE t) T
            source
            theorem CommutingRepetition.VN.Modular.cbfc_congr_ae {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {G H : ℝ → ℂ} (hG : BorelCalc.CBdd G) (hH : BorelCalc.CBdd H) (h : ∀ (ξ : K), G =ᵐ[BorelCalc.ν E hE ξ] H) :
            BorelCalc.cbfc E hE G = BorelCalc.cbfc E hE H

            cbfc only sees the spectral measures.

            source
            theorem CommutingRepetition.VN.Modular.cbfc_comp_trunc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {G : ℝ → ℂ} (hG : BorelCalc.CBdd G) (hGc : Continuous G) :
            (BorelCalc.cbfc E hE fun (l : ℝ) => G (trunc E l)) = BorelCalc.cbfc E hE G

            A continuous bounded function may be truncated: cbfc E (G ∘ trunc E) = cbfc E G.

            Clamped representatives of exponentials #

            clamp, continuous_clamp, abs_clamp_le, bdd_clamp and clamp_eq_of_abs_le come from VN/Modular/LinearRN.lean.

            source
            theorem CommutingRepetition.VN.Modular.trunc_eq_clamp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (E : K →L[ℂ] K) :
            trunc E = clamp ‖E‖
            source
            theorem CommutingRepetition.VN.Modular.abs_le_of_mem_spectrum {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} {l : ℝ} (hl : l ∈ spectrum ℝ E) :
            |l| ≤ ‖E‖
            source
            theorem CommutingRepetition.VN.Modular.bfc_clamp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {C : ℝ} (hC : ‖E‖ ≤ C) :
            BorelCalc.bfc E hE (clamp C) = E
            source
            theorem CommutingRepetition.VN.Modular.continuous_exp_clamp (r C : ℝ) :
            Continuous fun (l : ℝ) => Real.exp (r * clamp C l)

            l ↦ e^{r·clamp C l} is a bounded Borel function.

            source
            theorem CommutingRepetition.VN.Modular.bdd_exp_clamp (r : ℝ) {C : ℝ} (hC : 0 ≤ C) :
            BorelCalc.Bdd fun (l : ℝ) => Real.exp (r * clamp C l)
            source
            theorem CommutingRepetition.VN.Modular.expA_eq_bfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {C : ℝ} (hC : ‖E‖ ≤ C) (r : ℝ) :
            expA E r = BorelCalc.bfc E hE fun (l : ℝ) => Real.exp (r * clamp C l)

            The clamped representative of e^{rE} in the bounded Borel calculus.

            source
            theorem CommutingRepetition.VN.Modular.sub_eq_jbfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a b : K →L[ℂ] K} (hsa : IsSelfAdjoint a) (hsb : IsSelfAdjoint b) (hab : Commute a b) :
            b - a = BorelCalc.jbfc a b hsa hsb hab fun (p : ℝ × ℝ) => trunc b p.2 - trunc a p.1

            b − a as a joint Borel function of the commuting pair (a, b).

            source
            theorem CommutingRepetition.VN.Modular.bdd2_sub_trunc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a b : K →L[ℂ] K} :
            BorelCalc.Bdd2 fun (p : ℝ × ℝ) => trunc b p.2 - trunc a p.1
            source
            theorem CommutingRepetition.VN.Modular.continuous_sub_trunc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a b : K →L[ℂ] K} :
            Continuous fun (p : ℝ × ℝ) => trunc b p.2 - trunc a p.1
            source
            theorem CommutingRepetition.VN.Modular.cbdd_eitf_trunc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (E : K →L[ℂ] K) (t : ℝ) :
            BorelCalc.CBdd fun (l : ℝ) => eitf t (trunc E l)
            source
            theorem CommutingRepetition.VN.Modular.eit_sub {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a b : K →L[ℂ] K} (hsa : IsSelfAdjoint a) (hsb : IsSelfAdjoint b) (hab : Commute a b) (t : ℝ) :
            eit (b - a) ⋯ t = eit b hsb t * eit a hsa (-t)

            e^{it(b − a)} = e^{itb} e^{−ita} for commuting self-adjoint a, b.

            The product rule for exponentials of a commuting pair #

            source
            theorem CommutingRepetition.VN.Modular.clamp_nonneg_of_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a : K →L[ℂ] K} {C : ℝ} (hCa : ‖a‖ ≤ C) :
            0 ≤ C
            source
            theorem CommutingRepetition.VN.Modular.bdd2_clamp_sub {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a : K →L[ℂ] K} {C : ℝ} (hCa : ‖a‖ ≤ C) :
            BorelCalc.Bdd2 fun (p : ℝ × ℝ) => clamp C p.2 - clamp C p.1
            source
            theorem CommutingRepetition.VN.Modular.continuous_clamp_sub {C : ℝ} :
            Continuous fun (p : ℝ × ℝ) => clamp C p.2 - clamp C p.1
            source
            theorem CommutingRepetition.VN.Modular.abs_clamp_sub_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a : K →L[ℂ] K} {C : ℝ} (hCa : ‖a‖ ≤ C) (p : ℝ × ℝ) :
            |clamp C p.2 - clamp C p.1| ≤ 2 * C
            source
            theorem CommutingRepetition.VN.Modular.sub_eq_jbfc_clamp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a b : K →L[ℂ] K} (hsa : IsSelfAdjoint a) (hsb : IsSelfAdjoint b) (hab : Commute a b) {C : ℝ} (hCa : ‖a‖ ≤ C) (hCb : ‖b‖ ≤ C) :
            b - a = BorelCalc.jbfc a b hsa hsb hab fun (p : ℝ × ℝ) => clamp C p.2 - clamp C p.1

            b − a as a joint Borel function of the commuting pair (a, b), with a common clamp.

            source
            theorem CommutingRepetition.VN.Modular.expA_sub {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {a b : K →L[ℂ] K} (hsa : IsSelfAdjoint a) (hsb : IsSelfAdjoint b) (hab : Commute a b) {C : ℝ} (hCa : ‖a‖ ≤ C) (hCb : ‖b‖ ≤ C) (r : ℝ) :
            expA (b - a) r = expA b r * expA a (-r)

            e^{r(b − a)} = e^{rb} e^{−ra} for commuting self-adjoint a, b.