mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a

Tactic:
rw [← setIntegral_condKernel a MeasurableSet.univ ht hf]

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ

Tactic:
by
  conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
  rw [setLIntegral_compProd hf hs ht]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ

Tactic:
by
  rw [← setLIntegral_condKernel hf hs MeasurableSet.univ]; simp_rw [Measure.restrict_univ]

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
hi : ↑i ≤ a
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i

Tactic:
simp [hi]

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
hi : ¬↑i ≤ a
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i

Tactic:
simp [hi]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ (κ a) univ < (κ a) univ + 1

Tactic:
exact ENNReal.lt_add_right (measure_ne_top _ _) one_ne_zero

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

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)

Tactic:
refine ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, ?_⟩

Goal state after:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ (fun x ↦ f x.2) =ᵐ[Measure.map (fun ω ↦ (X ω, ω)) μ] fun x ↦ AEStronglyMeasurable.mk f hf x.2
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
⊢ {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u

Tactic:
intro t ht

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
t : γ
ht : t ∈ {x | (κ.fst a) (countablePartitionSet n x) = 0}
⊢ t ∈ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u}) = setBer(u, p) {s | i ∈ s}

Tactic:
simp [hi]

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measure.map (restrict₂ this) (Measure.map (frestrictLe (max (I.sup id) a)) ν) = μ I

pp: case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (restrict₂ this)

pp: case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (Iic (max (I.sup id) a)).restrict

pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ MeasurableSpace ((i : ↥(Iic (max (I.sup id) a))) → X ↑i)

Tactic:
h (le_max_right _ _),

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measure.map (restrict₂ this) (μ (Iic (max (I.sup id) a))) = μ I

case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (restrict₂ this)

case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (Iic (max (I.sup id) a)).restrict
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)

Tactic:
restrict₂

Goal state after:
case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc b c
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)

Tactic:
restrict₂

Goal state after:
case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc b c
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ (map (_root_.IicProdIoc a b) ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i))) (Set.univ.pi s) =
    ∏ i, (μ ↑i) (s i)

Tactic:
simp_rw [Measure.map_apply measurable_IicProdIoc (.univ_pi ms), IicProdIoc_preimage hab,
      Measure.prod_prod, Measure.pi_pi, prod_eq_prod_extend]

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x =
    ∏ x ≤ b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)

Tactic:
restrict₂

Goal state after:
case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)

Tactic:
restrict₂

Goal state after:
case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ (μ ↑⟨x, ⋯⟩) (s ⟨x, ⋯⟩) = (μ ↑⟨x, hx⟩) (s ⟨↑⟨x, hx⟩, ⋯⟩)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset x₀ (Iic (a + 1))
          (_root_.IicProdIoc a (a + 1) (frestrictLe a x₀, (piSingleton a) a_1))) ∂(κ a) (frestrictLe a x₀) =
    ∫⁻ (x : X (a + 1)), f (update x₀ (a + 1) x) ∂(κ a) (frestrictLe a x₀)

Tactic:
congrm ∫⁻ x, f (fun i ↦ ?_) ∂_
    simp only [updateFinset, mem_Iic, IicProdIoc_def, frestrictLe_apply, piSingleton,
      MeasurableEquiv.coe_mk, update]
    split_ifs with h1 h2 h3 <;> try rfl
    all_goals lia

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_sfinite _ _ hμ]; simp

Goal state after:
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 Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
this : μ ⊗ₘ κ ≪ μ.prod ν
⊢ Measure.map Prod.swap (μ ⊗ₘ κ) ≪ ν.prod μ

Tactic:
← Measure.prod_swap

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
this : μ ⊗ₘ κ ≪ μ.prod ν
⊢ Measure.map Prod.swap (μ ⊗ₘ κ) ≪ Measure.map Prod.swap (μ.prod ν)
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 : ℕ
hab : a ≤ b
n : ℕ
⊢ (traj κ b ∘ₖ partialTraj κ a b).map (frestrictLe n) = partialTraj κ a n

Tactic:
rw [map_comp, traj_map_frestrictLe, partialTraj_comp_partialTraj' _ hab]

Goal state after:
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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (map (⇑(piCongrLeft X e)) (infinitePi fun i ↦ μ (e i))) ((⇑e '' ↑(s.preimage ⇑e ⋯)).pi t) = ∏ i ∈ s, (μ i) (t i)

Tactic:
rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]

Goal state after:
case hst
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ (i : α), i ∈ s.preimage ⇑e ⋯ ↔ e i ∈ s

case hfg
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ i ∈ s.preimage ⇑e ⋯, (μ (e i)) (t (e i)) = (μ (e i)) (t (e i))

case mt
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ i ∈ s.preimage ⇑e ⋯, MeasurableSet (t (e i))

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable ⇑(piCongrLeft X e)

case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ MeasurableSet ((⇑e '' ↑(s.preimage ⇑e ⋯)).pi t)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: case refine_1
Ω : 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)
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) < ∞

Tactic:
calc ∫⁻ x, (κ†μ).rnDeriv (Kernel.const _ μ) x.2 x.1 ∂μ.prod (κ ∘ₘ μ)
    _ = (μ ⊗ₘ κ) Set.univ := by rw [← setLIntegral_univ, ← Set.univ_prod_univ, h1 .univ .univ]
    _ < ⊤ := measure_lt_top _ _

Goal state after:
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ avgRisk ℓ P κ π = ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x ∂⇑P ∘ₘ π

Tactic:
rw [avgRisk_eq_lintegral_posterior_prod hl, Measure.lintegral_bind (by fun_prop) (by fun_prop)]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (a : 𝓧), ∫⁻ (x : Θ × 𝓨), ℓ x.1 x.2 ∂(P†π ×ₖ κ) a ∂⇑P ∘ₘ π =
    ∫⁻ (x : 𝓧), ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x ∂⇑P ∘ₘ π
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π ≤ avgRisk ℓ P κ π

Tactic:
by
  rw [avgRisk_eq_lintegral_lintegral_lintegral hl]
  gcongr with x
  exact iInf_le_lintegral _

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

Goal state before:
pp: case h
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ ∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂Measure.map (frestrictLe b) ((traj κ a) x₀), Integrable f ((traj κ b) y)

Tactic:
· convert! i_f.1
      rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a

Tactic:
exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

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)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
⊢ IsProbabilityMeasure (trajMeasure μ₀ κ)

Tactic:
rw [trajMeasure]
  have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piUnique ((fun i : Iic 0 ↦ X i))).symm) :=
    Measure.isProbabilityMeasure_map <| by fun_prop
  infer_instance

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false.mpr
p : ℝ≥0
h : p ≤ 1
h' : p = 1
⊢ 1 - ↑p = 0

Tactic:
simp only [h', ENNReal.coe_one, tsub_self]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : iIndepFun X P
this : IsProbabilityMeasure P
⊢ map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P

Tactic:
have _ i := isProbabilityMeasure_map (mX.eval i)

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : iIndepFun X P
this : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
⊢ map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
⊢ iIndepFun X P

Tactic:
have _ i := isProbabilityMeasure_map (mX.eval i)

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
⊢ iIndepFun X P