OAI/LinearAlgebra/MatrixState/Whitening.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RowColumn.MatrixState.stateMean line 12
2. def OAI.RowColumn.MatrixState.whitenState line 14
3. lemma OAI.RowColumn.MatrixState.stateMean_positive line 17
4. lemma OAI.RowColumn.MatrixState.smul_le_stateMean line 23
5. lemma OAI.RowColumn.MatrixState.stateMean_trace_le_one line 28
6. lemma OAI.RowColumn.MatrixState.mean_support line 38
7. lemma OAI.RowColumn.MatrixState.whitenState_positive line 46
8. lemma OAI.RowColumn.MatrixState.stateMean_whiten line 51
9. lemma OAI.RowColumn.MatrixState.unwhitenState line 60
10. lemma OAI.RowColumn.MatrixState.stateMean_even line 65
11. lemma OAI.RowColumn.MatrixState.sqrt_even line 72
12. lemma OAI.RowColumn.MatrixState.quarter_even line 79
13. lemma OAI.RowColumn.MatrixState.inverseQuarter_even line 83
14. lemma OAI.RowColumn.MatrixState.whitenState_even line 89
15. lemma OAI.RowColumn.MatrixState.independent_overlap_mean line 103

    Source documentation

    The independent marginal mean of the local squared Hilbert--Schmidt factors, with no invertibility assumption on either average state.

    lemma independent_overlap_mean (p : L → ℝ) (q : K → ℝ)
        (S : L → Matrix C C ℂ) (T : K → Matrix C C ℂ) (U : Matrix C C ℂ) :
        (∑ i, ∑ j, p i * q j * (S i * U * T j * U.conjTranspose).trace.re) =
          (stateMean p S * U * stateMean q T * U.conjTranspose).trace.re := by
    …

    Mentions: OAI.RowColumn.MatrixState.stateMean

16. theorem OAI.RowColumn.MatrixState.weighted_whitened_mean_le_one line 122

    Source documentation

    Quarter-root whitening makes the independent mean at most one, while preserving singular substates exactly on every occupied fibre.

    theorem weighted_whitened_mean_le_one (p : L → ℝ) (q : K → ℝ)
        (S : L → Matrix C C ℂ) (T : K → Matrix C C ℂ)
        (hp : ∀ i, 0 ≤ p i) (hq : ∀ j, 0 ≤ q j)
        (hpsum : ∑ i, p i = 1) (hqsum : ∑ j, q j = 1)
        (hS : ∀ i, (S i).PosSemidef) (hT : ∀ j, (T j).PosSemidef)
        (hStr : ∀ i, (S i).trace.re ≤ 1) (hTtr : ∀ j, (T j).trace.re ≤ 1)
        (U : Matrix C C ℂ) (hU : U ∈ unitary (Matrix C C ℂ)) :
        (∑ i, ∑ j, p i * q j *
          (whitenState (stateMean p S) (S i) * U *
            whitenState (stateMean q T) (T j) * U.conjTranspose).trace.re) ≤ 1 := by
    …

    Mentions: OAI.RowColumn.MatrixState.whitenState, OAI.RowColumn.MatrixState.stateMean

17. lemma OAI.RowColumn.MatrixState.local_overlap_nonneg line 137