OAI/Analysis/FiniteFactor/Fiber/ProjectionDiagonal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.fiberProjection_diagonal_inner line 10

   Source documentation

   The diagonal of an orthogonal projection is the square norm of its column.

   theorem fiberProjection_diagonal_inner (P : SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
       (hp : IsStarProjection P) (k : ℤ) :
       P (lp.single 2 k (1 : ℂ)) k =
         inner ℂ (P (lp.single 2 k (1 : ℂ))) (P (lp.single 2 k (1 : ℂ))) := by
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert

2. theorem OAI.FiniteFactor.fiberProjection_diagonal_zero_iff line 22
3. theorem OAI.FiniteFactor.fiberProjection_diagonal_one_iff line 27
4. theorem OAI.FiniteFactor.fiberProjection_diagonal_bounds line 37
5. theorem OAI.FiniteFactor.fiberProjection_range_coordinate_zero line 55

   Source documentation

   If a diagonal entry is zero, that coordinate annihilates the entire range.

   theorem fiberProjection_range_coordinate_zero (P : SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
       (hp : IsStarProjection P) (k : ℤ) (hz : P (lp.single 2 k (1 : ℂ)) k = 0)
       (v : SourceFiberHilbert) : P v k = 0 := by
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert

6. theorem OAI.FiniteFactor.fiberProjection_diagonal_implications line 66

   Source documentation

   Positivity of the diagonal weight transfers zero backwards and one forwards.

   theorem fiberProjection_diagonal_implications
       (P Q D : SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
       (hp : IsStarProjection P) (hq : IsStarProjection Q)
       (hi : (1-Q)*D*P = 0) (a : ℂ) (ha : a ≠ 0)
       (hd : ∀ v : SourceFiberHilbert, D v 0 = a * v 0)
       (he : D (lp.single 2 0 (1 : ℂ)) = a • lp.single 2 0 (1 : ℂ)) :
       (Q (lp.single 2 0 (1 : ℂ)) 0 = 0 → P (lp.single 2 0 (1 : ℂ)) 0 = 0) ∧
       (P (lp.single 2 0 (1 : ℂ)) 0 = 1 → Q (lp.single 2 0 (1 : ℂ)) 0 = 1) := by
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert