OAI/Probability/SKRatio/Calculus/FieldTails.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Calculus.reversal line 13
2. lemma OAI.SKRatio.Calculus.reversal_reversal line 15
3. lemma OAI.SKRatio.Calculus.spin_reversal line 19
4. lemma OAI.SKRatio.Calculus.mass_reversal line 23
5. lemma OAI.SKRatio.Calculus.field_reversal line 29
6. lemma OAI.SKRatio.Calculus.gibbsMean_field_zero line 33
7. lemma OAI.SKRatio.Calculus.halfDiff_field line 42
8. lemma OAI.SKRatio.Calculus.unweightedGradient_field line 50
9. lemma OAI.SKRatio.Calculus.stationary_field_variance_le line 54
10. lemma OAI.SKRatio.Calculus.field_mean_of_overlap line 74
11. lemma OAI.SKRatio.Calculus.exp_abs_le_sum line 93
12. lemma OAI.SKRatio.Calculus.indicator_max_le_exp line 100
13. lemma OAI.SKRatio.Calculus.semigroup_max_tail line 131
14. theorem OAI.SKRatio.Calculus.uniform_field_tails_of_moments line 165