OAI/Probability/FreeIsing/Spectral/SpectralTransfer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.selfAdjoint_pow_norm_sq_le line 13
2. lemma OAI.Problem367.selfAdjoint_norm_pow_two_pow_le line 25
3. lemma OAI.Problem367.selfAdjoint_norm_apply_le_of_unit_power_bound line 40
4. lemma OAI.Problem367.selfAdjoint_norm_apply_le_of_power_bound line 58
5. lemma OAI.Problem367.selfAdjoint_norm_apply_le_on_closure_of_power_bound line 79
6. lemma OAI.Problem367.selfAdjoint_opNorm_le_of_dense_power_bound line 92
7. lemma OAI.Problem367.selfAdjoint_opNorm_le_of_dense_even_moment_bound line 101
8. lemma OAI.Problem367.norm_pow_apply_le_of_intertwiner line 131
9. lemma OAI.Problem367.selfAdjoint_norm_apply_le_on_closure_range_of_intertwiner line 159
10. lemma OAI.Problem367.selfAdjoint_opNorm_le_of_dense_intertwiner line 169