Theorems · Definition · probability

ProbabilityTheory.Kernel.Indep

{α : Type u_1} →
  {Ω : Type u_2} →
    {_mα : MeasurableSpace α} →
      MeasurableSpace Ω →
        MeasurableSpace Ω →
          {_mΩ : MeasurableSpace Ω} →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.Indep._auto_1 → Prop

Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a kernel κ and a measure μ if for any sets t₁ ∈ m₁, t₂ ∈ m₂, ∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)

Defined in

Mathlib.Probability.Independence.Kernel.Indep

Cited by

42 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound