OAI/Probability/SKGap/Gaussian/ReplicaTailWeight.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.replicaTailWeight line 22
2. def OAI.SKGapCutoff.replicaTail line 26
3. lemma OAI.SKGapCutoff.replicaTailWeight_nonneg line 30
4. lemma OAI.SKGapCutoff.replicaTail_eq_ratio line 38
5. lemma OAI.SKGapCutoff.replicaTail_nonneg line 51
6. lemma OAI.SKGapCutoff.replicaTailWeight_le_partition_sq line 56
7. lemma OAI.SKGapCutoff.replicaTail_le_one line 67
8. lemma OAI.SKGapCutoff.integrable_replicaTailWeight line 72
9. lemma OAI.SKGapCutoff.integral_replicaTailWeight line 84
10. lemma OAI.SKGapCutoff.replicaTailWeight_annealed_identity line 107
11. lemma OAI.SKGapCutoff.sign_square_tail_le line 125
12. lemma OAI.SKGapCutoff.replicaTailWeight_annealed_bound line 161
13. lemma OAI.SKGapCutoff.probability_markov_real line 173
14. lemma OAI.SKGapCutoff.scalar_log_ratio_tail line 183
15. lemma OAI.SKGapCutoff.divide_exponential_scalar line 201
16. lemma OAI.SKGapCutoff.replicaTail_probability_transfer line 207
17. lemma OAI.SKGapCutoff.replicaTail_disorder_probability_bound line 242
18. lemma OAI.SKGapCutoff.replica_overlap_vanishes line 281