OAI/Probability/FreeIsing/Spectral/RealChebyshevBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.chebyshev_pell line 8
2. lemma OAI.Problem367.isSelfAdjoint_aeval_real line 26
3. lemma OAI.Problem367.commute_aeval_self line 38
4. lemma OAI.Problem367.selfAdjoint_inner_square line 46
5. lemma OAI.Problem367.norm_le_one_of_pell line 51
6. lemma OAI.Problem367.norm_aeval_chebyshev_T_le_real line 85
7. lemma OAI.Problem367.norm_aeval_chebyshev_U_le_real line 100