BanditRLProof.KernelIndependentExtension

Restricting both coordinates of a semidirect product is the semidirect product of the restricted base measure and restricted fiber kernel.

theorem compProd_restrict_prod {A B : Type*} [MeasurableSpace A] [MeasurableSpace B] (mu : Measure A) [SFinite mu] (kernel : Kernel A B) [IsSFiniteKernel kernel] {s : Set A} {t : Set B} (hs : MeasurableSet s) (ht : MeasurableSet t) : (mu ⊗ₘ kernel).restrict (s ×ˢ t) = mu.restrict s ⊗ₘ kernel.restrict ht

A semidirect-product law restricted to a measurable safe set depends only on the base law on a measurable base safe set and on each kernel's restriction to the corresponding safe fiber.

theorem compProd_restrict_eq_of_base_restrict_eq_of_fiber_restrict_eq {A B : Type*} [MeasurableSpace A] [MeasurableSpace B] {mu nu : Measure A} [SFinite mu] [SFinite nu] {kernel eta : Kernel A B} [IsSFiniteKernel kernel] [IsSFiniteKernel eta] {baseSafe : Set A} {safe : Set (A × B)} (hbaseSafe : MeasurableSet baseSafe) (hsafe : MeasurableSet safe) (hsafe_base : safe ⊆ baseSafe ×ˢ Set.univ) (hbase : mu.restrict baseSafe = nu.restrict baseSafe) (hfiber : ∀ a ∈ baseSafe, (kernel a).restrict (Prod.mk a ⁻¹' safe) = (eta a).restrict (Prod.mk a ⁻¹' safe)) : (mu ⊗ₘ kernel).restrict safe = (nu ⊗ₘ eta).restrict safe

Mapped form of `compProd_restrict_eq_of_base_restrict_eq_of_fiber_restrict_eq`: a measurable successor map preserves the safe-set equality.

theorem map_compProd_restrict_eq_of_base_restrict_eq_of_fiber_restrict_eq {A B C : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] {mu nu : Measure A} [SFinite mu] [SFinite nu] {kernel eta : Kernel A B} [IsSFiniteKernel kernel] [IsSFiniteKernel eta] (successor : A × B → C) (hsuccessor : Measurable successor) {baseSafe : Set A} {successorSafe : Set C} (hbaseSafe : MeasurableSet baseSafe) (hsuccessorSafe : MeasurableSet successorSafe) (hpreimage_base : successor ⁻¹' successorSafe ⊆ baseSafe ×ˢ Set.univ) (hbase : mu.restrict baseSafe = nu.restrict baseSafe) (hfiber : ∀ a ∈ baseSafe, (kernel a).restrict (Prod.mk a ⁻¹' (successor ⁻¹' successorSafe)) = (eta a).restrict (Prod.mk a ⁻¹' (successor ⁻¹' successorSafe))) : ((mu ⊗ₘ kernel).map successor).restrict successorSafe = ((nu ⊗ₘ eta).map successor).restrict successorSafe

Pull independence on a pushforward measure back along the measurable map that produced that pushforward.

theorem IndepFun.comp_of_map {Omega Sample X Y : Type*} [MeasurableSpace Omega] [MeasurableSpace Sample] [MeasurableSpace X] [MeasurableSpace Y] {mu : Measure Omega} {z : Omega -> Sample} {x : Sample -> X} {y : Sample -> Y} (hz : Measurable z) (hx : Measurable x) (hy : Measurable y) (hindep : IndepFun x y (mu.map z)) : IndepFun (x ∘ z) (y ∘ z) mu

If `x` is independent of `past`, adjoining a Markov-kernel output whose law only depends on `past` leaves `x` independent of that output.

theorem indepFun_fst_snd_compProd_comap_of_indepFun {Omega X Past Output : Type*} [MeasurableSpace Omega] [MeasurableSpace X] [MeasurableSpace Past] [MeasurableSpace Output] (mu : Measure Omega) [IsProbabilityMeasure mu] (x : Omega -> X) (hx : Measurable x) (past : Omega -> Past) (hpast : Measurable past) (kernel : Kernel Past Output) [IsMarkovKernel kernel] (hindep : IndepFun x past mu) : IndepFun (x ∘ Prod.fst) Prod.snd (mu ⊗ₘ kernel.comap past hpast)

If `x` is independent of `past`, adjoining an output through a finite kernel that only sees `past` gives the joint output/`x` law as the output marginal times the original `x` marginal. Unlike the preceding `IndepFun` wrapper, this statement remains valid for subprobability kernels such as a branch-restricted Markov kernel.

theorem map_snd_x_compProd_comap_eq_prod_map_of_indepFun {Omega X Past Output : Type*} [MeasurableSpace Omega] [MeasurableSpace X] [MeasurableSpace Past] [MeasurableSpace Output] (mu : Measure Omega) [IsProbabilityMeasure mu] (x : Omega -> X) (hx : Measurable x) (past : Omega -> Past) (hpast : Measurable past) (kernel : Kernel Past Output) [IsFiniteKernel kernel] (hindep : IndepFun x past mu) : Measure.map (fun sample : Omega × Output => (sample.2, x sample.1)) (mu ⊗ₘ kernel.comap past hpast) = (Measure.map Prod.snd (mu ⊗ₘ kernel.comap past hpast)).prod (Measure.map x mu)