OAI/Probability/InvariantIsing/Fields/CascadeSeedCoupling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.ancestor_fiber_map_product line 14

   Source documentation

   Replacing a mark by a seed realization and replacing each descendant law by the same conditional law preserves the full marked subtree distribution.

   lemma ancestor_fiber_map_product {S A B C D : Type*}
       [MeasurableSpace S] [MeasurableSpace A] [MeasurableSpace B]
       [MeasurableSpace C] [MeasurableSpace D]
       (P : Measure S) (μ : Measure A) (Q : Measure B) (R : Measure C)
       [IsProbabilityMeasure P] [IsProbabilityMeasure μ]
       [IsProbabilityMeasure Q] [IsProbabilityMeasure R]
       {f : S → A} (hf : Measurable f) (hlaw : P.map f = μ)
       {g : A × B → D} {h : A × C → D} (hg : Measurable g) (hh : Measurable h)
       (hsub : ∀ a, Q.map (fun b => g (a,b)) = R.map (fun c => h (a,c))) :
       (P.prod Q).map (fun p => (f p.1,g (f p.1,p.2))) =
         (μ.prod R).map (fun p => (p.1,h p)) := by
   …