OAI/Analysis/KadisonSimilarity/Derivation/DicksonDischarge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact norm-two row and column estimate, with the little Grothendieck inequality obtained from norm-attaining states and matrix dilation.

  1. theorem OAI.KadisonSimilarity.dicksonTwoBound_proved line 15

    Source documentation

    Dickson (2014), Lemma 2.9, equation (19), for the native rectangular norms.

    theorem dicksonTwoBound_proved : DicksonTwoBound (A := A) H :=
…

    Mentions: OAI.KadisonSimilarity.DicksonTwoBound