OAI/Analysis/KadisonKastler/ConcreteScalarRecovery.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_left_polar_with_support line 23

   Source documentation

   Concrete polar decomposition supplies the support data required by the tracial compression identity.

   theorem exists_left_polar_with_support (x : Algebra M) :
       ∃ w : Algebra M,
         x = CFC.sqrt (x * star x) * w ∧ IsStarProjection (w * star w) ∧
         (w * star w) * CFC.sqrt (x * star x) = CFC.sqrt (x * star x) ∧
         CFC.sqrt (x * star x) * (w * star w) = CFC.sqrt (x * star x) := by
   …

   Mentions: OAI.KadisonKastler.Algebra

2. theorem OAI.KadisonKastler.concrete_traceOneNorm_scaled_projection_compression line 43

   Source documentation

   Polar decomposition gives the projection-compression identity for concrete von Neumann algebras.

   theorem concrete_traceOneNorm_scaled_projection_compression
       (τ : FaithfulTracialState (Algebra M)) (n : ℕ) (p e a : Algebra M)
       (hp : IsStarProjection p) (he : IsStarProjection e) :
       (n : ℝ) * traceOneNorm τ (p * e * a * e * p) =
         traceOneNorm τ (CFC.sqrt ((n : ℂ) • (e * p * e)) * a *
           CFC.sqrt ((n : ℂ) • (e * p * e))) := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceOneNorm

3. theorem OAI.KadisonKastler.concrete_recovery_scalar_at_least_half line 56

   Source documentation

   Two spectral tail estimates bound the real part of the recovered scalar below by one half.

   theorem concrete_recovery_scalar_at_least_half
       (τ : FaithfulTracialState (Algebra M)) {n N : ℕ} (hn : 0 < n)
       (hsize : 100 * (n : ℝ) * (100 * Real.pi) ^ 3 ≤ N)
       (p f e : Algebra M) (hp : IsStarProjection p) (he : IsStarProjection e)
       (hpτ : τ.toLinearMap p = (((n : ℝ)⁻¹ : ℝ) : ℂ))
       (heτ : τ.toLinearMap e = ((100 / (N : ℝ) : ℝ) : ℂ))
       (hmom : CenteredProjectionMoments τ p e (n : ℝ)⁻¹ (100 / N))
       (hf : ‖f * f‖ ≤ N)
       (htail : (n : ℝ) * traceOneNorm τ
         (recoveryCompression p f - p * e * (f * f) * e * p) ≤
           Real.pi / (100 * Real.pi))
       (hmass : 1 - Real.pi / (100 * Real.pi) ≤ traceOneNorm τ (e * (f * f) * e)) :
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CenteredProjectionMoments, OAI.KadisonKastler.traceOneNorm, OAI.KadisonKastler.recoveryCompression