OAI/Probability/SKGap/Brownian/WorstContinuousFieldMgf.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.worstContinuous_le_of_field_mgf line 146
2. lemma OAI.SKGapCutoff.abs_gibbsExpectation_le line 182
3. lemma OAI.SKGapCutoff.semigroup_abs_centered_le_gradient line 188
4. lemma OAI.SKGapCutoff.field_gibbs_centered line 207
5. lemma OAI.SKGapCutoff.exponential_envelope_integral line 211
6. lemma OAI.SKGapCutoff.exponential_envelope_mgf line 226