BoundaryPolarTrace.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Tracial continuity of the near-identity polar factor

The proof uses the trace pairing and the norm bound on each positive polar factor. It does not require a measurable functional-calculus selection or an operator-topology continuity theorem.

theorem OAI.KadisonKastler.FaithfulTracialState.re_star_mul_selfAdjoint line 21
Source documentation
In a tracial state, taking the adjoint of one factor does not change the real pairing with a selfadjoint factor.
```
theorem FaithfulTracialState.re_star_mul_selfAdjoint (τ : FaithfulTracialState B)
    (y p : B) (hp : IsSelfAdjoint p) :
    (τ.toLinearMap (star y * p)).re = (τ.toLinearMap (y * p)).re := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.FaithfulTracialState.norm_square_pairing_le line 31
Source documentation
A trace estimate for one bounded right factor.
```
theorem FaithfulTracialState.norm_square_pairing_le (τ : FaithfulTracialState B)
    (x d : B) : ‖τ.toLinearMap (star x * x * d)‖ ≤ ‖d‖ * traceTwoNorm τ x ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.polar_trace_pairing_identity line 41

Source documentation

Exact real trace identity underlying the polar Lipschitz estimate.

theorem polar_trace_pairing_identity (τ : FaithfulTracialState B)
    (u v : unitary B) (p q : B) (hp : IsSelfAdjoint p) (hq : IsSelfAdjoint q) :
    2 * (τ.toLinearMap (star ((u : B) - (v : B)) * ((u : B) * p - (v : B) * q))).re =
      (τ.toLinearMap (star ((u : B) - (v : B)) * ((u : B) - (v : B)) * (p + q))).re := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState

theorem OAI.KadisonKastler.polar_traceTwoNorm_bound_of_factors line 77

Source documentation

Positive polar factors within radius r of one give a tracial Lipschitz bound, with no commutation requirement between the factors.

theorem polar_traceTwoNorm_bound_of_factors (τ : FaithfulTracialState B)
    (u v : unitary B) (p q : B) (hp : IsSelfAdjoint p) (hq : IsSelfAdjoint q)
    {r : ℝ} (hpn : ‖p - 1‖ ≤ r) (hqn : ‖q - 1‖ ≤ r) :
    (1 - r) * traceTwoNorm τ ((u : B) - (v : B)) ≤
      traceTwoNorm τ ((u : B) * p - (v : B) * q) := by
…

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

theorem OAI.KadisonKastler.polar_traceTwoNorm_lipschitz line 116

Source documentation

Near-identity unitary polar factors are Lipschitz for the faithful tracial two-norm.

theorem polar_traceTwoNorm_lipschitz (τ : FaithfulTracialState B)
    (b c : B) (u v : unitary B)
    (hu : (u : B) * CFC.abs b = b) (hv : (v : B) * CFC.abs c = c)
    {r : ℝ} (hr : r < 1) (hb : ‖b - 1‖ ≤ r) (hc : ‖c - 1‖ ≤ r) :
    (1 - r) * traceTwoNorm τ ((u : B) - (v : B)) ≤ traceTwoNorm τ (b - c) := by
…

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

theorem OAI.KadisonKastler.polar_traceTwoNorm_le_inv_mul line 136

Source documentation

The explicit Lipschitz constant on a fixed neighborhood of one.

theorem polar_traceTwoNorm_le_inv_mul (τ : FaithfulTracialState B)
    (b c : B) (u v : unitary B)
    (hu : (u : B) * CFC.abs b = b) (hv : (v : B) * CFC.abs c = c)
    {r : ℝ} (hr : r < 1) (hb : ‖b - 1‖ ≤ r) (hc : ‖c - 1‖ ≤ r) :
    traceTwoNorm τ ((u : B) - (v : B)) ≤ (1 - r)⁻¹ * traceTwoNorm τ (b - c) := by
…

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