OAI/MeasureTheory/DyadicAvoidance/RoutedSetDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem310.RoutedSetDensity.selectorChoice line 17

   Source documentation

   The actual first-success/default child choice made by the finite selector tables.

   def selectorChoice {M d : ℕ} (b : Node M d → Fin M → ℕ)
       (ω : SelectorTable b) (P : List (Child M)) (x : ℝ) : Child M :=
   …

2. def OAI.Problem310.RoutedSetDensity.routedLeaf line 22

   Source documentation

   The leaf reached by the root router, as an element of the finite leaf type.

   def routedLeaf {M d : ℕ} (b : Node M d → Fin M → ℕ)
       (ω : SelectorTable b) (x : ℝ) : Leaf M d :=
   …

3. def OAI.Problem310.RoutedSetDensity.routedAddress line 27

   Source documentation

   The terminal table coordinate consulted by the complete finite router.

   def routedAddress {M d : ℕ} (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
       (ω : SelectorTable bS) (x : ℝ) : TerminalAddress bT :=
   …

4. def OAI.Problem310.RoutedSetDensity.routedSet line 32

   Source documentation

   The raw random periodic set, with both selector and terminal tables explicit.

   def routedSet {M d : ℕ} (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
       (ω : SelectorTable bS × TerminalTable bT) : Set ℝ :=
   …

5. lemma OAI.Problem310.RoutedSetDensity.measurable_selectorChoice line 36
6. lemma OAI.Problem310.RoutedSetDensity.selectorChoice_add_one line 42
7. lemma OAI.Problem310.RoutedSetDensity.measurable_routedLeaf line 49
8. lemma OAI.Problem310.RoutedSetDensity.routedLeaf_add_one line 64
9. lemma OAI.Problem310.RoutedSetDensity.measurable_routedAddress line 69
10. lemma OAI.Problem310.RoutedSetDensity.routedAddress_add_one line 75
11. lemma OAI.Problem310.RoutedSetDensity.measurableSet_routedSet line 80
12. lemma OAI.Problem310.RoutedSetDensity.routedSet_periodic line 85
13. theorem OAI.Problem310.RoutedSetDensity.expected_routedSet_density line 91

    Source documentation

    Exact density of the concrete raw routed blocker, with no spatial regularity hypotheses.

    theorem expected_routedSet_density {M d : ℕ} (bS : Node M d → Fin M → ℕ)
        (bT : Leaf M d → ℕ) (P : Measure (SelectorTable bS)) [IsProbabilityMeasure P]
        (ν : Measure Bool) [IsProbabilityMeasure ν] :
        (∫⁻ ω, volume (routedSet bS bT ω ∩ Set.Icc (0 : ℝ) 1)
          ∂(P.prod (Measure.pi (fun _ : TerminalAddress bT => ν)))) = ν {true} := by
    …

    Mentions: OAI.Problem310.RoutedSetDensity.routedSet