OAI/Analysis/OperatorAlgebra/HypertraceFiniteDensity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The convex separation step in the finite hypertrace argument. An invariant state can be approximated on a prescribed finite set by finite vector functionals whose conjugation defects are small in the predual norm. This is norm control of the defects, not merely weak convergence.

  1. abbrev OAI.WeakPureInfiniteness.HypertraceTestSpace line 20
  2. instance OAI.WeakPureInfiniteness.hypertraceTestNormed line 24
  3. instance OAI.WeakPureInfiniteness.hypertraceTestReal line 27
  4. instance OAI.WeakPureInfiniteness.hypertraceTestBounded line 30
  5. instance OAI.WeakPureInfiniteness.hypertraceTestContinuousSMul line 33
  6. def OAI.WeakPureInfiniteness.hypertraceVectorTest line 36
  7. def OAI.WeakPureInfiniteness.hypertraceStateTest line 41
  8. def OAI.WeakPureInfiniteness.testScalarPart line 44
  9. def OAI.WeakPureInfiniteness.testPredualPart line 47
  10. lemma OAI.WeakPureInfiniteness.testFunctional_expansion line 52
  11. lemma OAI.WeakPureInfiniteness.operator_realPart_quadratic line 66
  12. lemma OAI.WeakPureInfiniteness.conjugatedOperator_inner line 76
  13. theorem OAI.WeakPureInfiniteness.hypertraceStateTest_mem_closure line 81
  14. def OAI.WeakPureInfiniteness.finiteVectorDensity line 131
  15. theorem OAI.WeakPureInfiniteness.hypertrace_finite_density line 137

    Source documentation

    Simultaneous finite state tests and norm-small conjugation defects. This is the finite-rank density step used before the Powers--Størmer estimate.

    theorem hypertrace_finite_density (T : I → H →L[ℂ] H)
    (hT : ∀ i, IsSelfAdjoint (T i)) (U : J → H ≃ₗᵢ[ℂ] H)
    (φ : (H →L[ℂ] H) →ₚ[ℂ] ℂ) (hφ : φ 1 = 1)
    (hU : ∀ j A, φ (conjugatedOperator (U j) A) = φ A)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (n : ℕ) (w : Fin n → ℝ) (x : Fin n → H),
      (∀ k, 0 ≤ w k) ∧ (∑ k, w k = 1) ∧ (∀ k, ‖x k‖ ≤ 1) ∧
      (∀ i, |(φ (T i)).re - ∑ k, w k * (inner ℂ (x k) (T i (x k))).re| < ε) ∧
      ∀ j, ‖finitePredualUnitary (U j) (finiteVectorDensity w x) - finiteVectorDensity w x‖ < ε := by
…

    Mentions: OAI.WeakPureInfiniteness.conjugatedOperator, OAI.WeakPureInfiniteness.finitePredualUnitary, OAI.WeakPureInfiniteness.finiteVectorDensity