OAI/Probability/SKGap/Localization/SemigroupAbs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.semigroup_abs_le_one line 141
2. lemma OAI.SKGapCutoff.halfDiff_abs_le_one line 150
3. lemma OAI.SKGapCutoff.backward_energy_budget line 157
4. lemma OAI.SKGapCutoff.gradient_le_energy_bad line 178
5. lemma OAI.SKGapCutoff.backward_gradient_energy_bound line 202
6. lemma OAI.SKGapCutoff.gradient_bound_from_backward_energy line 225
7. lemma OAI.SKGapCutoff.worstContinuous_le_of_backward_energy line 265