OAI/NumberTheory/JointDickman/Probability/SitePartition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.mergeSitePartition line 14
2. theorem OAI.JointDickman.mergeSitePartition_restrict line 19
3. theorem OAI.JointDickman.siteProductMass_merge line 26
4. theorem OAI.JointDickman.siteProduct_partition line 45

   Source documentation

   The exposed endpoint block is integrated outside the independent law of all remaining sites. No probability of the exposed event is divided out.

   theorem siteProduct_partition (p : ι → Ω → ℝ) (I : Finset ι) (F : (ι → Ω) → ℝ) :
       finiteExpectation (siteProductMass p) F =
         finiteExpectation (siteProductMass (fun i : I => p i.val)) (fun a =>
           finiteExpectation (siteProductMass (fun i : {i : ι // i ∉ I} => p i.val))
             (fun b => F (mergeSitePartition I a b))) := by
   …

   Mentions: OAI.JointDickman.finiteExpectation, OAI.JointDickman.mergeSitePartition