Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.Kernel.finiteSupport_of_compProd'

PFR.ForMathlib.Entropy.Kernel.Basic · PFR/ForMathlib/Entropy/Kernel/Basic.lean:72 to 83

Source documentation

Composing a finitely supported measure with a finitely supported kernel gives a finitely supported kernel.

Exact Lean statement

lemma finiteSupport_of_compProd' [MeasurableSingletonClass S] [MeasurableSingletonClass T]
    {μ : Measure T} [IsFiniteMeasure μ] {κ : Kernel T S}
    [IsZeroOrMarkovKernel κ] [FiniteSupport μ] (hκ : FiniteKernelSupport κ) :
    FiniteSupport (μ ⊗ₘ κ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma finiteSupport_of_compProd' [MeasurableSingletonClass S] [MeasurableSingletonClass T]    {μ : Measure T} [IsFiniteMeasure μ] {κ : Kernel T S}    [IsZeroOrMarkovKernel κ] [FiniteSupport μ] (hκ : FiniteKernelSupport κ) :    FiniteSupport (μ ⊗ₘ κ) := by  let A := μ.support  have hA := measure_compl_support μ  rcases (local_support_of_finiteKernelSupport hκ A) with ⟨B, hB⟩  use A ×ˢ B  rw [Measure.ae_compProd_iff (by exact (Finset.finite_toSet _).measurableSet)]  filter_upwards [ae_mem_support μ] with t ht  filter_upwards [hB t ht] with s hs  exact Finset.mk_mem_product ht hs