OAI/Probability/SKGap/Brownian/ObservationPathEstimate.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.ObservationBridge.brownian_fixed_time_probability line 15
2. def OAI.SKGap.ObservationBridge.conditionalPathFailure line 34
3. def OAI.SKGap.ObservationBridge.pathFailure line 40
4. def OAI.SKGap.ObservationBridge.meshCertificate line 44
5. lemma OAI.SKGap.ObservationBridge.measurable_meshCertificate line 47
6. lemma OAI.SKGap.ObservationBridge.meshCertificate_nonneg line 52
7. lemma OAI.SKGap.ObservationBridge.fixedTimeFailure_as_sum line 57
8. theorem OAI.SKGap.ObservationBridge.observation_path_certificate line 69
9. lemma OAI.SKGap.ObservationBridge.partitionSizeBias_integral line 112
10. lemma OAI.SKGap.ObservationBridge.weighted_meshCertificate_integrable line 120
11. lemma OAI.SKGap.ObservationBridge.weighted_meshCertificate_integral line 127
12. theorem OAI.SKGap.ObservationBridge.quenched_observation_path_stability line 137