mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔ CondIndepSets m' hm' {s | MeasurableSet s} {s | MeasurableSet s} μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ ∫⁻ (x : X) in A ∩ B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X) in A, f x ∂π x₀

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Measurable Prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
⊢ (fun ω s ↦ X s ω) ⟂ᵢ[P] U

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : X✝.carrier × PUnit.{u + 1}
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ Measurable Prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ } ≫
      (let f₁ := fun x ↦ (x, PUnit.unit);
        have hf₁ := ⋯;
        have hf₂ := ⋯;
        { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom =
    (let f₁ := fun x ↦ (x, PUnit.unit);
        have hf₁ := ⋯;
        have hf₂ := ⋯;
        { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ }, inv := { hom := Kernel.id.map f₁, property := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom ≫
      κ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔ iCondIndep m' hm' (fun i ↦ generateFrom {s i}) μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Measurable id

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Measurable ⇑prodAssoc

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hs : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepSet m' hm' s t μ ↔ CondIndep m' (generateFrom {s}) (generateFrom {t}) hm' μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepSet m' hm' s t μ ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepFun m' hm' f μ ↔ iCondIndep m' hm' (fun x ↦ MeasurableSpace.comap (f x) (m x)) μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepFun m' hm' f μ ↔
    ∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω ↦ 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ {
        hom :=
          { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                  inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                  inv_hom_id := ⋯ }.hom.hom ∥ₖ
            Kernel.id,
        property := ⋯ } ≫
      { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
            inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        {
          hom :=
            Kernel.id ∥ₖ
              { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
                    inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ }.hom.hom,
          property := ⋯ } =
    { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepFun m' hm' f g μ ↔ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable id

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable Prod.snd

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable Prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable (Prod.snd ∘ id)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable (Prod.fst ∘ id)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      {
        hom :=
          Kernel.id ∥ₖ
            (let f₁ := fun x ↦ (PUnit.unit, x);
                have hf₁ := ⋯;
                have hf₂ := ⋯;
                { hom := { hom := Kernel.id.map Prod.snd, property := ⋯ },
                  inv := { hom := Kernel.id.map f₁, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom.hom,
        property := ⋯ } =
    {
      hom :=
        (let f₁ := fun x ↦ (x, PUnit.unit);
              have hf₁ := ⋯;
              have hf₂ := ⋯;
              { hom := { hom := Kernel.id.map Prod.fst, property := ⋯ },
                inv := { hom := Kernel.id.map f₁, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }).hom.hom ∥ₖ
          Kernel.id,
      property := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] fun ω ↦
            μ[(f ⁻¹' s).indicator fun ω ↦ 1 | m'] ω * μ[(g ⁻¹' t).indicator fun ω ↦ 1 | m'] ω

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap X.carrier Y.carrier)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap Y.carrier X.carrier)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ X ⊗ Y ≅ Y ⊗ X

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
κ : Y ⟶ Z
⊢ X ◁ κ ≫
      { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      κ ▷ X

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
X : SFinKer
⊢ κ ▷ X ≫
      { hom := { hom := Kernel.swap Y✝.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier Y✝.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    { hom := { hom := Kernel.swap X✝.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier X✝.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      X ◁ κ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ (α_ X Y Z).hom ≫
      { hom := { hom := Kernel.swap X.carrier (Y ⊗ Z).carrier, property := ⋯ },
            inv := { hom := Kernel.swap (Y ⊗ Z).carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        (α_ Y Z X).hom =
    { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ▷
        Z ≫
      (α_ Y X Z).hom ≫
        Y ◁
          { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
⊢ ∀ i ∈ s, sets i = f i ⁻¹' g i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ iCondIndepFun m' hm' f μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
⊢ ∫⁻ (x : X), g x * f x ∂π x₀ = g x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
s : X
x y : ↑I
hxy : x ≤ y
⊢ Icc 0 x ⊆ Icc 0 y

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ (α_ X Y Z).inv ≫
      { hom := { hom := Kernel.swap (X ⊗ Y).carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier (X ⊗ Y).carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        (α_ Z X Y).inv =
    X ◁
        { hom := { hom := Kernel.swap Y.carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      (α_ X Z Y).inv ≫
        { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ▷
          Y

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[(X ⁻¹' s).indicator 1 * (Y ⁻¹' t).indicator 1 | m'] =ᵐ[μ] (X ⁻¹' s).indicator 1 * μ[(Y ⁻¹' t).indicator 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    𝟙 (X ⊗ Y)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    𝟙 (X ⊗ Y)

Tactic:
by
    ext : 1; simp

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ IsSFiniteKernel (Kernel.discard X.carrier)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ IsSFiniteKernel (Kernel.copy X.carrier)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Measurable fun x ↦ (PUnit.unit, x)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ { hom := Kernel.copy X.carrier, property := ⋯ } ≫ { hom := Kernel.discard X.carrier, property := ⋯ } ▷ X = (λ_ X).inv

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Measurable fun x ↦ (x, PUnit.unit)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ { hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.discard X.carrier, property := ⋯ } = (ρ_ X).inv

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ (X ⁻¹' s).indicator 1 * μ[(Y ⁻¹' t).indicator 1 | m'] =ᵐ[μ]
    μ[(X ⁻¹' s).indicator 1 | m'] * μ[(Y ⁻¹' t).indicator 1 | m']

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ { hom := Kernel.copy X.carrier, property := ⋯ } ≫ X ◁ { hom := Kernel.copy X.carrier, property := ⋯ } =
    { hom := Kernel.copy X.carrier, property := ⋯ } ≫
      { hom := Kernel.copy X.carrier, property := ⋯ } ▷ X ≫ (α_ X X X).hom

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ Measurable fun p ↦ f p.1 * g p.2

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
⊢ CondIndepFun m' hm' X Y μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Δ ≫ (β_ X X).hom = Δ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
⊢ CondIndepFun m' hm' X Y μ

Tactic:
by
  rw [condIndepFun_iff _ hm' _ _ (hX.mono hm' le_rfl) hY]
  rintro _ _ ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
  rw [show (fun ω : Ω ↦ (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]
  calc μ[(X ⁻¹' s).indicator 1 * (Y ⁻¹' t).indicator 1 | m']
  _ =ᵐ[μ] (X ⁻¹' s).indicator 1 * μ[(Y ⁻¹' t).indicator 1 | m'] := by
    refine condExp_stronglyMeasurable_mul_of_bound hm' (stronglyMeasurable_const.indicator (hX hs))
      ((integrable_indicator_iff (hY ht)).2 integrableOn_const) 1 (ae_of_all μ fun ω ↦ ?_)
    rw [Set.indicator]
    split_ifs with h <;> simp
  _ =ᵐ[μ] μ[(X ⁻¹' s).indicator 1 | m'] * μ[(Y ⁻¹' t).indicator 1 | m'] := by
    nth_rw 2 [condExp_of_stronglyMeasurable hm']
    · exact stronglyMeasurable_const.indicator (hX hs)
    · exact (integrable_indicator_iff ((hX.le hm') hs)).2 integrableOn_const

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
⊢ Z ⟂ᵢ[P] U

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : CountableOrCountablyGenerated Ω (β × β')
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    ⇑((condExpKernel μ m').map fun ω ↦ (f ω, g ω)) =ᵐ[μ.trim hm']
      ⇑((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
q : ℚ
hqa : ↑a < ↑q
hqI : 0 ≤ q ∧ ↑q ≤ 1
h : (κ e.1).real (Icc 0 ⟨↑q, ⋯⟩) < ↑e.2
⊢ 0 ≤ ↑q

Tactic:
by

Goal state after: