OAI/Analysis/MatrixSigning/Calculus/NormSmulRightId.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Calculus.norm_smulRight_id_le line 22
2. lemma OAI.CurrentKS.Calculus.JetBound.smul_const line 29
3. lemma OAI.CurrentKS.Calculus.norm_apply_bilinear_le line 35
4. lemma OAI.CurrentKS.Calculus.JetBound.apply line 43
5. lemma OAI.CurrentKS.Calculus.norm_comp_contractions line 51