OAI/MeasureTheory/DyadicAvoidance/FirstDefault.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem310.FirstDefault.Address line 13
2. abbrev OAI.Problem310.FirstDefault.Path line 14
3. abbrev OAI.Problem310.FirstDefault.Tests line 15
4. def OAI.Problem310.FirstDefault.pathPrefix line 18

   Source documentation

   The node immediately before the kth decision along a nondefault path.

   def pathPrefix {M d : ℕ} (f : Path M d) (k : Fin d) : List (Fin (M + 1)) :=
   …

   Mentions: OAI.Problem310.FirstDefault.Path

5. lemma OAI.Problem310.FirstDefault.pathPrefix_eq_take_ofFn line 21
6. def OAI.Problem310.FirstDefault.address line 26

   Source documentation

   Every earlier rejected selector and the selected selector are tested.

   def address {M d : ℕ} (f : Path M d) (i : Tests f) : Address M :=
   …

   Mentions: OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.Tests, OAI.Problem310.FirstDefault.Address

7. def OAI.Problem310.FirstDefault.requiredBit line 29
8. def OAI.Problem310.FirstDefault.cylinder line 33

   Source documentation

   The selector cylinder expressing that a prescribed path is followed.

   def cylinder {M d : ℕ} {Ω : Type u_Ω} (S : Address M → Ω → Bool)
       (f : Path M d) : Set Ω :=
   …

   Mentions: OAI.Problem310.FirstDefault.Address, OAI.Problem310.FirstDefault.Path

9. lemma OAI.Problem310.FirstDefault.address_injective line 37
10. lemma OAI.Problem310.FirstDefault.measure_cylinder_of_local line 50
11. lemma OAI.Problem310.FirstDefault.measure_cylinder line 68
12. lemma OAI.Problem310.FirstDefault.cylinder_disjoint_of_prefix line 77
13. lemma OAI.Problem310.FirstDefault.cylinders_pairwiseDisjoint line 98
14. lemma OAI.Problem310.FirstDefault.measurableSet_cylinder line 124
15. lemma OAI.Problem310.FirstDefault.sum_geometric_weights line 130
16. theorem OAI.Problem310.FirstDefault.measure_no_default line 154

    Source documentation

    Probability that a full depth-d center path never chooses the default child. The event is expressed as the union of its explicit nondefault path cylinders.

    theorem measure_no_default {M d : ℕ} {Ω : Type u_Ω} [MeasurableSpace Ω]
        (μ : Measure Ω) (S : Address M → Ω → Bool)
        (hS : ∀ a, Measurable (S a)) (hIndep : iIndepFun S μ)
        (hfair : ∀ a b, μ (S a ⁻¹' {b}) = (2 : ENNReal)⁻¹) :
        μ (⋃ f : Path M d, cylinder S f) =
          (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
    …

    Mentions: OAI.Problem310.FirstDefault.Address, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.cylinder

17. theorem OAI.Problem310.FirstDefault.measure_no_default_of_local line 171

    Source documentation

    Local independence suffices: only the finitely many addresses on each prescribed path are required to be independent and fair.

    theorem measure_no_default_of_local {M d : ℕ} {Ω : Type u_Ω} [MeasurableSpace Ω]
        (μ : Measure Ω) (S : Address M → Ω → Bool)
        (hS : ∀ a, Measurable (S a))
        (hIndep : ∀ f : Path M d, iIndepFun (fun i : Tests f => S (address f i)) μ)
        (hfair : ∀ f : Path M d, ∀ i : Tests f, ∀ b,
          μ (S (address f i) ⁻¹' {b}) = (2 : ENNReal)⁻¹) :
        μ (⋃ f : Path M d, cylinder S f) =
          (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
    …

    Mentions: OAI.Problem310.FirstDefault.Address, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.Tests, OAI.Problem310.FirstDefault.address, OAI.Problem310.FirstDefault.cylinder

18. abbrev OAI.Problem310.FirstDefault.BoundedAddress line 188
19. lemma OAI.Problem310.FirstDefault.address_length_lt line 190
20. def OAI.Problem310.FirstDefault.boundedAddress line 194
21. lemma OAI.Problem310.FirstDefault.boundedAddress_injective line 197
22. theorem OAI.Problem310.FirstDefault.measure_no_default_bounded line 204

    Source documentation

    Finite-tree version: no randomness outside nodes of depth less than d is assumed. This is the interface for the actual finite table model.

    theorem measure_no_default_bounded {M d : ℕ} {Ω : Type u_Ω} [MeasurableSpace Ω]
        (μ : Measure Ω) (S : BoundedAddress M d → Ω → Bool)
        (hS : ∀ a, Measurable (S a)) (hIndep : iIndepFun S μ)
        (hfair : ∀ a b, μ (S a ⁻¹' {b}) = (2 : ENNReal)⁻¹) :
        μ (⋃ f : Path M d,
          {ω | ∀ i : Tests f, S (boundedAddress f i) ω = requiredBit f i}) =
          (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d := by
    …

    Mentions: OAI.Problem310.FirstDefault.BoundedAddress, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.Tests, OAI.Problem310.FirstDefault.boundedAddress, OAI.Problem310.FirstDefault.requiredBit