OAI/RepresentationTheory/RowColumn/CopyOverlap.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RowColumn.hilbertSchmidtSq line 18

   Source documentation

   Ordinary squared Hilbert--Schmidt norm on a possibly rectangular map.

   def hilbertSchmidtSq (B : V →L[ℂ] W) : ℝ :=
   …

2. lemma OAI.RowColumn.hilbertSchmidtSq_eq_sum line 21
3. lemma OAI.RowColumn.norm_sq_le_hilbertSchmidtSq line 29
4. def OAI.RowColumn.copyProjection line 61

   Source documentation

   Sum of the genuine range projections for the given isometric copies.

   def copyProjection (I : Fin u → V →ₗᵢ[ℂ] X) : X →L[ℂ] X :=
   …

5. lemma OAI.RowColumn.hilbertSchmidtSq_overlap line 64
6. lemma OAI.RowColumn.allCopy_hilbertSchmidt_identity line 79

   Source documentation

   The all-copy identity in weighted.tex:126–133, for the actual embeddings. No overlap bound is an assumption.

   lemma allCopy_hilbertSchmidt_identity (I : Fin u → V →ₗᵢ[ℂ] X)
       (J : Fin v → W →ₗᵢ[ℂ] X) :
       ∑ i, ∑ j, hilbertSchmidtSq
         ((I i).toContinuousLinearMap.adjoint.comp (J j).toContinuousLinearMap) =
       (LinearMap.trace ℂ X ((copyProjection I).comp (copyProjection J)).toLinearMap).re := by
   …

   Mentions: OAI.RowColumn.hilbertSchmidtSq, OAI.RowColumn.copyProjection

7. lemma OAI.RowColumn.allCopyOverlap_le_trace line 96
8. lemma OAI.RowColumn.isometry_adjoint_apply line 126
9. lemma OAI.RowColumn.isometry_adjoint_comp line 133
10. lemma OAI.RowColumn.copyProjection_positive line 138
11. lemma OAI.RowColumn.copyProjection_trace line 144
12. lemma OAI.RowColumn.copyProjection_intertwines line 159
13. lemma OAI.RowColumn.allCopyOverlap_comp_isometry line 172
14. lemma OAI.RowColumn.allCopyOverlap_le_count line 189
15. lemma OAI.RowColumn.isometric_adjoint_intertwines line 225
16. def OAI.RowColumn.gramIntertwiner line 233
17. theorem OAI.RowColumn.isometric_intertwiner_of_injective line 244

    Source documentation

    Every actual nonzero algebraic embedding of irreducible unitary carriers normalizes to an isometric intertwiner. No normalized embedding is assumed.

    theorem isometric_intertwiner_of_injective [Representation.IsIrreducible ρ]
        (f : Representation.IntertwiningMap ρ τ) (hf : Function.Injective f) :
        ∃ I : V →ₗᵢ[ℂ] E, ∀ g x, I (ρ g x)=τ g (I x) := by
    …