OAI/Probability/SKGap/Localization/FixedTimeQuenched.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.ObservationBridge.fixedTimeFailure line 14
2. lemma OAI.SKGap.ObservationBridge.measurable_fixedTimeFailure line 17
3. lemma OAI.SKGap.ObservationBridge.fixedTimeFailure_nonneg line 21
4. lemma OAI.SKGap.ObservationBridge.fixedTimeFailure_le_one line 24
5. lemma OAI.SKGap.ObservationBridge.ofReal_fixedTimeFailure line 29
6. lemma OAI.SKGap.ObservationBridge.disorder_partition_integrable line 34
7. def OAI.SKGap.ObservationBridge.partitionSizeBias line 42
8. lemma OAI.SKGap.ObservationBridge.partitionSizeBias_pos line 45
9. lemma OAI.SKGap.ObservationBridge.partitionSizeBias_integrable line 51
10. lemma OAI.SKGap.ObservationBridge.weighted_fixedTimeFailure_integrable line 55
11. lemma OAI.SKGap.ObservationBridge.weighted_fixedTimeFailure_integral_bound line 64
12. theorem OAI.SKGap.ObservationBridge.quenched_fixed_time_root_stability line 78