OAI/Probability/SKGap/Brownian/ContinuousEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.continuous_energy line 15
2. lemma OAI.SKGapCutoff.continuous_partition line 20
3. lemma OAI.SKGapCutoff.continuous_gibbs line 24
4. lemma OAI.SKGapCutoff.continuous_field line 29
5. lemma OAI.SKGapCutoff.continuous_mean line 34
6. lemma OAI.SKGapCutoff.continuous_siteVariance line 41
7. lemma OAI.SKGapCutoff.continuous_gibbsExpectation line 45
8. lemma OAI.SKGapCutoff.continuous_gibbsVariance line 51
9. lemma OAI.SKGapCutoff.continuous_dirichlet line 58
10. lemma OAI.SKGapCutoff.isClosed_hasGap line 65
11. lemma OAI.SKGapCutoff.continuous_sampledInteraction line 71
12. lemma OAI.SKGapCutoff.measurableSet_sampledGap line 83