OAI/Probability/SKGap/Terminal/TerminalMatrixMeasurable.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.continuous_coupling_entry line 14
2. lemma OAI.SKGap.continuous_coupling_matrix line 18
3. lemma OAI.SKGap.continuous_tanh_real line 24
4. lemma OAI.SKGap.continuous_terminalU line 27
5. lemma OAI.SKGap.continuous_terminalQ line 34
6. lemma OAI.SKGap.continuous_principalOperatorNorm line 41
7. lemma OAI.SKGap.terminalMatrixData_measurable line 46
8. lemma OAI.SKGap.nat_pow_exp_div_tendsto line 78
9. lemma OAI.SKGap.nat_pow_exp_sqrt_div_tendsto line 85
10. lemma OAI.SKGap.terminalRawTail_tendsto line 92
11. lemma OAI.SKGap.sparse_parameters line 115