OAI/Geometry/HyperbolicGroups/Conditioning.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.FiniteLaw.joinTables line 16
2. lemma OAI.HyperbolicObstruction.FiniteLaw.joinTables_in line 19
3. lemma OAI.HyperbolicObstruction.FiniteLaw.joinTables_out line 23
4. lemma OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct_mass_join line 29
5. lemma OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct_expect_split line 42
6. theorem OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct_event_mul line 62

   Source documentation

   Exact independence of an arbitrary outside-trial statistic from the event that every trial in S is present.

   theorem bernoulliProduct_event_mul (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1)
       (S : Finset I) (f : (I → Bool) → ℝ)
       (depends : ∀ w z, (∀ i, i ∉ S → w i = z i) → f w = f z) :
       (bernoulliProduct p hp).expect (fun w => if ∀ i ∈ S, w i = true then f w else 0) =
         (∏ i ∈ S, p i) * (bernoulliProduct p hp).expect f := by
   …

   Mentions: OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.FiniteLaw.expect