OAI/Analysis/FactorGeneration/LocalizedStates.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Localization of actual signed vector/dimension values. Fixed strict sublevel sets, rather than a limiting strict inequality, supply Zorn bounds.

  1. theorem OAI.Generator.Tracial.AlgebraProjection.exists_nonnegative_corner line 22

    Source documentation

    A continuous orthogonally additive real charge nonnegative on G admits a nonzero corner all of whose subprojections have nonnegative charge.

    theorem exists_nonnegative_corner
    (μ : AlgebraProjection M → ℝ)
    (hadd : ∀ p q (ho : p.val*q.val=0), μ (orthogonalSum p q ho)=μ p+μ q)
    (hcont : ∀ (I : Type u) [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
      (a : I → AlgebraProjection M), Monotone a →
      ∀ p, IsLUB (Set.range a) p → Tendsto (fun i => μ (a i)) atTop (𝓝 (μ p)))
    (G : AlgebraProjection M) (hG : G.val≠0) (hμG : 0 ≤ μ G) :
    ∃ F : AlgebraProjection M, F ≤ G ∧ F.val≠0 ∧ ∀ p, p ≤ F → 0 ≤ μ p := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.orthogonalSum

  2. theorem OAI.Generator.Tracial.traceFreeDimension_tendsto_monotone line 83
  3. theorem OAI.Generator.Tracial.exists_signed_vector_dimension_corner line 97

    Source documentation

    Concrete localization for a real linear combination of the actual vector functional and the already constructed dimension; no linear trace is assumed.

    theorem exists_signed_vector_dimension_corner
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (ξ : H) (c d : ℝ) (G : AlgebraProjection M) (hG : G.val≠0)
    (hμG : 0 ≤ c*G.vectorValue ξ+d*traceFreeDimension hfactor hdiff G) :
    ∃ F : AlgebraProjection M, F ≤ G ∧ F.val≠0 ∧
      ∀ p, p ≤ F → 0 ≤ c*p.vectorValue ξ+d*traceFreeDimension hfactor hdiff p := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  4. theorem OAI.Generator.Tracial.exists_vector_dimension_lower_corner line 121
  5. theorem OAI.Generator.Tracial.exists_vector_dimension_upper_corner line 132
  6. theorem OAI.Generator.Tracial.exists_vector_dimension_localization line 158

    Source documentation

    An actual unit vector admits a nonzero corner on which every projection value is between a D(p) and (1+ε)a D(p), with a strictly positive.

    theorem exists_vector_dimension_localization
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (ξ : H) (hξ : ‖ξ‖=1) (ε : ℝ) (hε : 0<ε) :
    ∃ (E : AlgebraProjection M) (a : ℝ), E.val≠0 ∧ 0<a ∧
      ∀ p : AlgebraProjection M, p ≤ E →
        a*traceFreeDimension hfactor hdiff p ≤ (inner ℂ ξ (p.val.val ξ)).re ∧
        (inner ℂ ξ (p.val.val ξ)).re ≤ (1+ε)*a*traceFreeDimension hfactor hdiff p := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

  7. def OAI.Generator.Tracial.vectorFunctional line 239

    Source documentation

    The actual bounded complex-linear vector functional on the original algebra.

    def vectorFunctional (ξ : H) : M.toStarSubalgebra →L[ℂ] ℂ :=
…
  8. theorem OAI.Generator.Tracial.vectorFunctional_apply line 249
  9. theorem OAI.Generator.Tracial.vectorFunctional_norm_le line 252
  10. theorem OAI.Generator.Tracial.exists_positive_corner_spectral_approximation line 256

    Source documentation

    A positive operator supported by p is approximated inside that same corner.

    theorem exists_positive_corner_spectral_approximation
    (p : AlgebraProjection M) (x : M.toStarSubalgebra) (hx : 0 ≤ x)
    (hpx : p.val*x=x) (ε : ℝ) (hε : 0<ε) :
    ∃ (Q : CornerPartition p) (c : Fin Q.size → ℝ),
      (∀ i, 0 ≤ c i) ∧ (∀ i, Commute (Q.piece i).val x) ∧
      ‖x-∑ i, (c i : ℂ) • (Q.piece i).val‖ < ε := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.Q, OAI.Generator.Tracial.CornerPartition

  11. theorem OAI.Generator.Tracial.IsDimensionSpectralValue.corner_bound line 293
  12. theorem OAI.Generator.Tracial.positive_functional_bounds_of_projection_bounds line 349
  13. theorem OAI.Generator.Tracial.exists_localized_vector_functional line 418

    Source documentation

    Concrete projection and positive-operator localization, with an actual bounded complex-linear functional and a nonzero constructed corner.

    theorem exists_localized_vector_functional
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (ξ : H) (hξ : ‖ξ‖=1) (ε : ℝ) (hε : 0<ε) :
    ∃ (E : AlgebraProjection M) (a : ℝ), E.val≠0 ∧ 0<a ∧
      ∀ (x : M.toStarSubalgebra) (hx : 0 ≤ x), E.val*x=x →
        a*(dimensionSpectralValue hfactor hdiff hfinite hunit x hx.isSelfAdjoint).re ≤
          (vectorFunctional ξ x).re ∧
        (vectorFunctional ξ x).re ≤
          (1+ε)*a*(dimensionSpectralValue hfactor hdiff hfinite hunit x hx.isSelfAdjoint).re := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.dimensionSpectralValue, OAI.Generator.Tracial.vectorFunctional

  14. theorem OAI.Generator.Tracial.exists_unit_vector_of_unit_ne_zero line 448
  15. theorem OAI.Generator.Tracial.vectorFunctional_star_mul_self line 463
  16. theorem OAI.Generator.Tracial.vectorFunctional_positive line 470
  17. theorem OAI.Generator.Tracial.vectorFunctional_one line 479
  18. theorem OAI.Generator.Tracial.exists_corner_nearly_cyclic_vector line 494

    Source documentation

    A localized vector functional is nearly cyclic for every element in its corner. This gives both inequalities by applying the result to x and x*.

    theorem exists_corner_nearly_cyclic_vector
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    (ξ : H) (hξ : ‖ξ‖=1) (ε : ℝ) (hε : 0<ε) :
    ∃ E : AlgebraProjection M, E.val≠0 ∧
      (∀ p : AlgebraProjection M, p ≤ E → p.val≠0 → 0<(vectorFunctional ξ p.val).re) ∧
      ∀ x : M.toStarSubalgebra, E.val*x=x → x*E.val=x →
        (vectorFunctional ξ (star x*x)).re ≤ (1+ε)*(vectorFunctional ξ (x*star x)).re := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.vectorFunctional

  19. theorem OAI.Generator.Tracial.exists_nearly_cyclic_corner_state line 525

    Source documentation

    Entirely constructed from the original finite diffuse factor fields: a positive unital bounded linear functional, and a nonzero nearly cyclic corner.

    theorem exists_nearly_cyclic_corner_state
    (hunit : (1 : M.toStarSubalgebra) ≠ 0) (ε : ℝ) (hε : 0<ε) :
    ∃ (φ : M.toStarSubalgebra →L[ℂ] ℂ) (E : AlgebraProjection M),
      ‖φ‖ ≤ 1 ∧ φ 1=1 ∧ (∀ x : M.toStarSubalgebra, 0 ≤ x → 0 ≤ (φ x).re) ∧
      E.val≠0 ∧ (∀ p : AlgebraProjection M, p ≤ E → p.val≠0 → 0<(φ p.val).re) ∧ ∀ x : M.toStarSubalgebra, E.val*x=x → x*E.val=x →
        (φ (star x*x)).re ≤ (1+ε)*(φ (x*star x)).re := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection

  20. theorem OAI.Generator.Tracial.EquivalentPartition.compose_base_target line 547
  21. def OAI.Generator.Tracial.EquivalentPartition.rebase line 555

    Source documentation

    Change the common initial corner by a displayed equivalence.

    def rebase (E : EquivalentPartition p ι) (v : PartialIsometry M) (hv : v.target=E.base) :
    EquivalentPartition p ι where
…

    Mentions: OAI.Generator.Tracial.EquivalentPartition, OAI.Generator.Tracial.PartialIsometry

  22. theorem OAI.Generator.Tracial.EquivalentPartition.base_ne_zero line 568
  23. theorem OAI.Generator.Tracial.EquivalentPartition.dimension_base line 591

    Source documentation

    Every actual finite equivalent partition has the expected base dimension.

    theorem EquivalentPartition.dimension_base
    (hunit : (1 : M.toStarSubalgebra) ≠ 0)
    {p : AlgebraProjection M} {ι : Type*} [Fintype ι] [Nonempty ι]
    (E : EquivalentPartition p ι) :
    traceFreeDimension hfactor hdiff E.base=traceFreeDimension hfactor hdiff p/Fintype.card ι := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.EquivalentPartition, OAI.Generator.Tracial.traceFreeDimension

  24. theorem OAI.Generator.Tracial.exists_equivalent_partition_base_le line 608

    Source documentation

    A partition of 1 with common initial projection inside any given nonzero E.

    theorem exists_equivalent_partition_base_le
    (hunit : (1 : M.toStarSubalgebra) ≠ 0) (E : AlgebraProjection M) (hE : E.val≠0) :
    ∃ (n : ℕ) (_hn : 0<n)
      (Q : EquivalentPartition (⟨1,IsStarProjection.one _⟩ : AlgebraProjection M) (Fin n)),
      Q.base ≤ E ∧ Q.base.val≠0 := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.Q, OAI.Generator.Tracial.EquivalentPartition

  25. def OAI.Generator.Tracial.EquivalentPartition.stateCoefficient line 648

    Source documentation

    Matrix coefficient in the common initial corner.

    def stateCoefficient (Q : EquivalentPartition p ι) (x : M.toStarSubalgebra) (i j : ι) :
    M.toStarSubalgebra := star (Q.leg i).val*x*(Q.leg j).val

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.EquivalentPartition

  26. theorem OAI.Generator.Tracial.EquivalentPartition.stateCoefficient_left line 651
  27. theorem OAI.Generator.Tracial.EquivalentPartition.stateCoefficient_right line 660
  28. theorem OAI.Generator.Tracial.EquivalentPartition.stateCoefficient_star line 666
  29. theorem OAI.Generator.Tracial.EquivalentPartition.stateCoefficient_mul line 670
  30. def OAI.Generator.Tracial.EquivalentPartition.matrixVectorFunctional line 681

    Source documentation

    An actual finite sum of bounded vector functionals.

    def matrixVectorFunctional (Q : EquivalentPartition p ι) (ξ : H) : M.toStarSubalgebra →L[ℂ] ℂ :=
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.EquivalentPartition

  31. theorem OAI.Generator.Tracial.EquivalentPartition.matrixVectorFunctional_apply line 684
  32. theorem OAI.Generator.Tracial.EquivalentPartition.matrixVectorFunctional_one line 694
  33. theorem OAI.Generator.Tracial.EquivalentPartition.matrixVectorFunctional_norm_le line 701
  34. theorem OAI.Generator.Tracial.EquivalentPartition.matrixVectorFunctional_nearly_cyclic line 710
  35. theorem OAI.Generator.Tracial.exists_approximately_tracial_state line 764

    Source documentation

    A constructed approximate tracial state on the entire original algebra.

    theorem exists_approximately_tracial_state
    (hunit : (1 : M.toStarSubalgebra) ≠ 0) (ε : ℝ) (hε : 0<ε) :
    ∃ φ : M.toStarSubalgebra →L[ℂ] ℂ,
      ‖φ‖ ≤ 1 ∧ φ 1=1 ∧ (∀ x : M.toStarSubalgebra, 0 ≤ x → 0 ≤ (φ x).re) ∧
      ∀ x : M.toStarSubalgebra, (φ (star x*x)).re ≤ (1+ε)*(φ (x*star x)).re := by
…