OAI/MeasureTheory/DyadicAvoidance/ChildDistribution.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.OrderedRouting.measure_chooseChild_default line 13

   Source documentation

   All nondefault selectors fail precisely on one product cylinder.

   theorem measure_chooseChild_default :
       Measure.pi (fun _ : Fin M => ν) {S | chooseChild S = Fin.last M} =
         (ν {false}) ^ M := by
   …

   Mentions: OAI.Problem310.OrderedRouting.chooseChild

2. theorem OAI.Problem310.OrderedRouting.measure_chooseChild_nondefault line 24

   Source documentation

   The first-success choice has the geometric child law.

   theorem measure_chooseChild_nondefault (i : Fin M) :
       Measure.pi (fun _ : Fin M => ν) {S | chooseChild S = i.castSucc} =
         ν {true} * (ν {false}) ^ i.val := by
   …

   Mentions: OAI.Problem310.OrderedRouting.chooseChild