Lean module · Probability layer
BanditRLProof.KernelIndependentExtension
# Independence through a past-measurable kernel extension This module records the semidirect-product transport needed by stochastic bandit trajectory laws. Sampling from a Markov kernel that only sees a past summary cannot create dependence between its output and a random variable already independent of that summary.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.IndepFun.comp_of_map
Compiled
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
theorem
BanditRLProof.indepFun_fst_snd_compProd_comap_of_indepFun
Compiled
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)