OAI/Combinatorics/UniformKServer/FiniteThreshold.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.FiniteThreshold.collapse line 15
2. def OAI.UniformKServer.FiniteThreshold.unitInterval line 23
3. instance OAI.UniformKServer.FiniteThreshold.unitInterval_probability line 25
4. def OAI.UniformKServer.FiniteThreshold.normalized line 28
5. theorem OAI.UniformKServer.FiniteThreshold.normalized_mem line 30
6. theorem OAI.UniformKServer.FiniteThreshold.normalized_measurable line 36
7. def OAI.UniformKServer.FiniteThreshold.threshold line 41
8. abbrev OAI.UniformKServer.FiniteThreshold.Signature line 43
9. def OAI.UniformKServer.FiniteThreshold.sample line 45
10. theorem OAI.UniformKServer.FiniteThreshold.sample_measurable line 48
11. def OAI.UniformKServer.FiniteThreshold.experiment line 67
12. theorem OAI.UniformKServer.FiniteThreshold.collapse_event line 69
13. theorem OAI.UniformKServer.FiniteThreshold.threshold_event line 78
14. theorem OAI.UniformKServer.FiniteThreshold.threshold_bool_event line 83
15. theorem OAI.UniformKServer.FiniteThreshold.interval_threshold line 92
16. theorem OAI.UniformKServer.FiniteThreshold.threshold_coordinate line 108

    Source documentation

    Finite collapse of one shared uniform threshold. These laws realize the same nested coverage events as a single truncated-exponential radius.

    theorem threshold_coordinate (p : X → ℝ) (hp : ∀ x, p x ∈ Set.Icc (0:ℝ) 1) (x : X) :
        (experiment p).expect (fun ω => if ω.val x then 1 else 0) = p x := by
    …

    Mentions: OAI.UniformKServer.FiniteThreshold.experiment

17. theorem OAI.UniformKServer.FiniteThreshold.threshold_hit line 113
18. theorem OAI.UniformKServer.FiniteThreshold.threshold_separation line 123