OAI/MeasureTheory/DyadicAvoidance/SelectedCoordinateLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.SelectedCoordinateLaw.measurePreserving_injective_coordinates line 13

   Source documentation

   Reading any injective family of coordinates of an iid finite table is measure preserving onto the corresponding smaller product table.

   theorem measurePreserving_injective_coordinates
       {I : Type u_I} {K : Type u_K} {B : Type u_B} [Fintype I] [Fintype K] [MeasurableSpace B]
       (ν : Measure B) [IsProbabilityMeasure ν]
       (addr : I → K) (hinj : Function.Injective addr) :
       MeasurePreserving (fun ω : K → B => fun i => ω (addr i))
         (Measure.pi (fun _ : K => ν)) (Measure.pi (fun _ : I => ν)) := by
   …