mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case h
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst✝¹ : SFinite μ
π : Measure Θ
inst✝ : SFinite π
hl_pos : μ Set.univ = ∞ → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0 → ∃ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
y : 𝓨
⊢ (∫⁻ (a : Θ), ℓ a y ∂π) * μ Set.univ ≤ (∫⁻ (θ : Θ), ℓ θ y ∂π) * μ Set.univ

pp: case h.hf
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst✝¹ : SFinite μ
π : Measure Θ
inst✝ : SFinite π
hl_pos : μ Set.univ = ∞ → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0 → ∃ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
y : 𝓨
⊢ Measurable fun θ ↦ ℓ θ y

Tactic:
]

Goal state after:
case h.hf
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst✝¹ : SFinite μ
π : Measure Θ
inst✝ : SFinite π
hl_pos : μ Set.univ = ∞ → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0 → ∃ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
y : 𝓨
⊢ Measurable fun θ ↦ ℓ θ y
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac✝ : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
ω : Ω
h_ac : κ ω ≪ ⇑κ ∘ₘ μ
⊢ (κ ω) t = (κ ω) t

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ partialTraj κ a b = partialTraj κ a b

pp: case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable (frestrictLe b)

pp: case hg
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable (restrict₂ ⋯)

Tactic:
]

Goal state after:
case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable (frestrictLe b)

case hg
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable (restrict₂ ⋯)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∏ i ∈ image Sigma.fst s, (infinitePi fun j ↦ μ i j) ((↑(s.preimage (Sigma.mk i) ⋯)).pi fun j ↦ t ⟨i, j⟩) =
    ∏ a ∈ image Sigma.fst s, ∏ s ∈ s.preimage (Sigma.mk a) ⋯, (μ ⟨a, s⟩.fst ⟨a, s⟩.snd) (t ⟨a, s⟩)

pp: case mt
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∀ i ∈ image Sigma.fst s, MeasurableSet ((↑(s.preimage (Sigma.mk i) ⋯)).pi fun j ↦ t ⟨i, j⟩)

Tactic:
]

Goal state after:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∏ i ∈ image Sigma.fst s, (infinitePi fun j ↦ μ i j) ((↑(s.preimage (Sigma.mk i) ⋯)).pi fun j ↦ t ⟨i, j⟩) =
    ∏ a ∈ image Sigma.fst s, ∏ s ∈ s.preimage (Sigma.mk a) ⋯, (μ ⟨a, s⟩.fst ⟨a, s⟩.snd) (t ⟨a, s⟩)

case mt
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∀ i ∈ image Sigma.fst s, MeasurableSet ((↑(s.preimage (Sigma.mk i) ⋯)).pi fun j ↦ t ⟨i, j⟩)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.fst p.snd) = infinitePi fun p ↦ μ p.fst p.snd

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm)
      (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)

pp: case hg
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable ⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)

pp: case hf
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable ⇑(MeasurableEquiv.curry ι κ X).symm

Tactic:
]

Goal state after:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm)
      (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)

case hg
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable ⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)

case hf
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable ⇑(MeasurableEquiv.curry ι κ X).symm
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.1 x.2 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
⊢ (μ ⊗ₘ κ) (Set.univ ×ˢ Set.univ) = (μ ⊗ₘ κ) (Set.univ ×ˢ Set.univ)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(MeasurableEquiv.curry ι κ X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) = infinitePi fun p ↦ μ p.1 p.2

Tactic:
rw [← (MeasurableEquiv.piCongrLeft (fun _ ↦ X)
    (Equiv.sigmaEquivProd ι κ).symm).map_measurableEquiv_injective.eq_iff, map_map]

Goal state after:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm)
      (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)

case hg
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable ⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)

case hf
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable ⇑(MeasurableEquiv.curry ι κ X).symm
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  ⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm =
    ⇑(piCurry fun x x_1 ↦ X).symm
⊢ (infinitePi fun p ↦ μ p.fst p.snd) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)

Tactic:
]

Goal state after:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  ⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm =
    ⇑(piCurry fun x x_1 ↦ X).symm
⊢ (infinitePi fun p ↦ μ p.fst p.snd) =
    map (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm)) (infinitePi fun p ↦ μ p.1 p.2)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.1 p.2) = infinitePi fun p ↦ μ p.1 p.2

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
⊢ Measure.map (fun x_1 ↦ updateFinset x_1 (Iic n) x) ((traj κ n) x) =
    ((Kernel.id ×ₖ (traj κ n).map (Set.Ioi n).domRestrict).map ⇑(IicProdIoi n)) x

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
⊢ Measure.map (fun x_1 ↦ updateFinset x_1 (Iic n) x) ((traj κ n) x) =
    ((Kernel.id ×ₖ (traj κ n).map (Set.Ioi n).domRestrict).map ⇑(IicProdIoi n)) x
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ (∫ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i) = ∫ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i

pp: case hφ
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEMeasurable s.restrict (infinitePi μ)

pp: case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.map s.restrict (infinitePi μ))

Tactic:
]

Goal state after:
case hφ
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEMeasurable s.restrict (infinitePi μ)

case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.map s.restrict (infinitePi μ))
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
π : Measure Θ
inst✝ : SFinite π
⊢ ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)

Tactic:
]

Goal state after:
case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
⊢ ⨅ x, avgRisk ℓ P (↑x) π = ⨅ x, avgRisk ℓ P (Kernel.const 𝓧 ↑x) π

Tactic:
]

Goal state after:
case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
⊢ ⨅ x, avgRisk ℓ P (↑x) π = ⨅ x, avgRisk ℓ P (Kernel.const 𝓧 ↑x) π
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
f : ((i : ↥s) → X ↑i) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : (i : ↥s) → X ↑i), f a ∂(fun I ↦ Measure.pi fun i ↦ μ ↑i) s =
    ∫⁻ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i

Tactic:
]

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

Goal state before:
pp: case refine_2
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.1 x.2 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
hs : MeasurableSet s
t : Set 𝓧
ht : MeasurableSet t
⊢ (μ ⊗ₘ κ) (s ×ˢ t) = (μ ⊗ₘ κ) (s ×ˢ t)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
e : { κ // IsMarkovKernel κ } ≃ { μ // IsProbabilityMeasure μ } :=
  { toFun := fun κ ↦ ⟨↑κ x, ⋯⟩, invFun := fun μ ↦ ⟨Kernel.const 𝓧 ↑μ, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ ⨅ x, avgRisk ℓ P (↑(e.symm x)) π = ⨅ x, avgRisk ℓ P (Kernel.const 𝓧 ↑x) π

Tactic:
]

Goal state after:
case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
e : { κ // IsMarkovKernel κ } ≃ { μ // IsProbabilityMeasure μ } :=
  { toFun := fun κ ↦ ⟨↑κ x, ⋯⟩, invFun := fun μ ↦ ⟨Kernel.const 𝓧 ↑μ, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ ⨅ x, avgRisk ℓ P (↑(e.symm x)) π = ⨅ x, avgRisk ℓ P (Kernel.const 𝓧 ↑x) π
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
⊢ ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π ≤ ⨅ μ, ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

Tactic:
]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
⊢ ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π ≤ ⨅ μ, ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝² : DecidableEq ι
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → E := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ (∫ (y : (i : ↥s) → X ↑i), g y ∂Measure.pi fun i ↦ μ ↑i) =
    ∫ (y : (i : ↥s) → X ↑i), f (Function.updateFinset x s y) ∂Measure.pi fun i ↦ μ ↑i

pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝² : DecidableEq ι
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → E := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ AEStronglyMeasurable g (Measure.pi fun i ↦ μ ↑i)

Tactic:
]

Goal state after:
case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝² : DecidableEq ι
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → E := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ AEStronglyMeasurable g (Measure.pi fun i ↦ μ ↑i)
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ ∫⁻ (y : Θ), ∫⁻ (x : 𝓨), ℓ y x * (P y) Set.univ ∂μ ∂π = ∫⁻ (θ : Θ), (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂μ ∂π

pp: case hf
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ AEMeasurable (uncurry fun x θ ↦ ℓ θ x * (P θ) Set.univ) (μ.prod π)

Tactic:
]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ ∫⁻ (y : Θ), ∫⁻ (x : 𝓨), ℓ y x * (P y) Set.univ ∂μ ∂π = ∫⁻ (θ : Θ), (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂μ ∂π

case hf
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ AEMeasurable (uncurry fun x θ ↦ ℓ θ x * (P θ) Set.univ) (μ.prod π)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (y : Ω) ∂μ, ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) y x

pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ MeasurableSet {x | (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.1 x.2 = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.2 x.1}

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (y : Ω) ∂μ, ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) y x

Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ MeasurableSet {x | (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.1 x.2 = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.2 x.1}