JointRelativeAverages.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous finite relative averages

Successively averaging two elements gives one finite family controlling both. The second average cannot increase the first element's tracial norm; its trace preserves the scalar target for the second element.

def OAI.KadisonKastler.relativeConjugationAverage line 23
Source documentation
Equal-weight conjugation by a finite family from the source algebra.
```
def relativeConjugationAverage {I : Type*} [Fintype I]
    (φ : R →⋆ₐ[ℂ] A) (u : I → unitary R) (a : A) : A :=
…
```
theorem OAI.KadisonKastler.trace_relativeConjugation line 27

theorem OAI.KadisonKastler.trace_relativeConjugationAverage line 39

Source documentation

Every finite relative average preserves the trace.

theorem trace_relativeConjugationAverage {I : Type*} [Fintype I] [Nonempty I]
    (τ : FaithfulTracialState A) (φ : R →⋆ₐ[ℂ] A) (u : I → unitary R) (a : A) :
    τ.toLinearMap (relativeConjugationAverage φ u a) = τ.toLinearMap a := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.relativeConjugationAverage

theorem OAI.KadisonKastler.traceTwoNorm_relativeConjugationAverage_le line 48

Source documentation

A finite relative average is contractive for the tracial two-norm.

theorem traceTwoNorm_relativeConjugationAverage_le {I : Type*}
    [Fintype I] [Nonempty I] (τ : FaithfulTracialState A)
    (J : A →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (φ : R →⋆ₐ[ℂ] A) (u : I → unitary R) (a : A) :
    traceTwoNorm τ (relativeConjugationAverage φ u a) ≤ traceTwoNorm τ a := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.relativeConjugationAverage

theorem OAI.KadisonKastler.relativeConjugationAverage_comp line 67

Source documentation

The Cartesian-product family implements composition of averages.

theorem relativeConjugationAverage_comp {I K : Type*} [Fintype I] [Fintype K]
    (φ : R →⋆ₐ[ℂ] A) (u : I → unitary R) (v : K → unitary R) (a : A) :
    relativeConjugationAverage φ (fun ki : K × I => v ki.1 * u ki.2) a =
      relativeConjugationAverage φ v (relativeConjugationAverage φ u a) := by
…

Mentions: OAI.KadisonKastler.relativeConjugationAverage

theorem OAI.KadisonKastler.traceTwoNorm_scalar_one line 79

theorem OAI.KadisonKastler.exists_joint_relative_averages_of_scalar line 86

Source documentation

Any scalar-averaging property supplies simultaneous two-norm bounds for two trace-bounded elements. No positivity assumption is needed.

theorem exists_joint_relative_averages_of_scalar
    (τ : FaithfulTracialState A) (J : A →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) (φ : R →⋆ₐ[ℂ] A)
    (havg : ∀ a : A, ∀ ε : ℝ, 0 < ε → ∃ n : ℕ, 0 < n ∧
      ∃ u : Fin n → unitary R,
        traceTwoNorm τ (relativeConjugationAverage φ u a -
          τ.toLinearMap a • (1 : A)) < ε)
    (a b : A) (ha : ‖τ.toLinearMap a‖ ≤ 1) (hb : ‖τ.toLinearMap b‖ ≤ 1) :
    ∃ n : ℕ, 0 < n ∧ ∃ u : Fin n → unitary R,
      traceTwoNorm τ (relativeConjugationAverage φ u a) ≤ 2 ∧
      traceTwoNorm τ (relativeConjugationAverage φ u b) ≤ 2 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.relativeConjugationAverage

theorem OAI.KadisonKastler.exists_joint_finite_relative_average line 141

Source documentation

In a concrete finite factor, irreducibility supplies one actual finite family simultaneously averaging any two trace-bounded elements.

theorem exists_joint_finite_relative_average
    (τ : FaithfulTracialState (Algebra M)) (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) (hτ : FiniteVectorTrace τ)
    (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (a b : Algebra M) (ha : ‖τ.toLinearMap a‖ ≤ 1) (hb : ‖τ.toLinearMap b‖ ≤ 1) :
    ∃ n : ℕ, 0 < n ∧ ∃ u : Fin n → unitary R,
      traceTwoNorm τ (relativeConjugationAverage φ u a) ≤ 2 ∧
      traceTwoNorm τ (relativeConjugationAverage φ u b) ≤ 2 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.relativeConjugationAverage