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

ProbabilityTheory.Kernel.local_support_of_finiteKernelSupport

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:686 to 699

Source documentation

Finite kernel support locally implies uniform finite kernel support.

Exact Lean statement

lemma local_support_of_finiteKernelSupport
    {κ : Kernel T S} (h : FiniteKernelSupport κ) (A : Finset T) :
    ∃ B : Finset S, ∀ t ∈ A, ∀ᵐ x ∂(κ t), x ∈ B

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma local_support_of_finiteKernelSupport    {κ : Kernel T S} (h : FiniteKernelSupport κ) (A : Finset T) :    ∃ B : Finset S, ∀ t ∈ A, ∀ᵐ x ∂(κ t), x ∈ B := by  classical  use A.biUnion (fun t ↦ (h t).choose)  intro t ht  change κ t (A.biUnion fun t ↦ (h t).choose)ᶜ = 0  set B := (h t).choose  refine measure_mono_null ?_ (h t).choose_spec  intro s  simp only [Finset.coe_biUnion, SetLike.mem_coe, Set.compl_iUnion, Set.mem_iInter,    Set.mem_compl_iff]  contrapose!; intro h  use t