OAI/Analysis/KadisonSimilarity/Representation/DenseFamilyIsometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Extend a map on a total family from its Gram matrix. This construction allows the family to have linear relations.

  1. theorem OAI.KadisonSimilarity.dense_span_of_scalar_tests line 18
  2. theorem OAI.KadisonSimilarity.inner_linearCombination_eq line 31
  3. theorem OAI.KadisonSimilarity.norm_linearCombination_eq line 39
  4. theorem OAI.KadisonSimilarity.denseRange_linearCombination line 50
  5. theorem OAI.KadisonSimilarity.continuousLinearMap_eq_zero_of_total line 59
  6. def OAI.KadisonSimilarity.denseFamilyIsometry line 73

    Source documentation

    The unique isometry sending a total family to a family with the same Gram matrix, constructed through finitely supported linear combinations.

    def denseFamilyIsometry (v : J → E) (w : J → F)
    (hv : (Submodule.span ℂ (Set.range v)).topologicalClosure = ⊤)
    (h : ∀ i j, inner ℂ (w i) (w j) = inner ℂ (v i) (v j)) : E →ₗᵢ[ℂ] F :=
…
  7. theorem OAI.KadisonSimilarity.denseFamilyIsometry_apply line 79