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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) ∂ρ.fst

Tactic:
have (a : _) : ρCond a (Prod.mk a ⁻¹' {x} ×ˢ s) = ({x} : Set α).indicator (ρCond · s) a := by
    obtain rfl | hax := eq_or_ne a x
    · simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]
      congr with y
      simp
    · simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_notMem]
      have : Prod.mk a ⁻¹' Prod.mk x '' s = ∅ := by ext y; simp [Ne.symm hax]
      simp only [this, measure_empty]

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this✝ : IsSFiniteKernel ρCond
this : ∀ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) ∂ρ.fst
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a = (κ a) (f' i)
h_eq : ∀ (a : β), Prod.mk a ⁻¹' ⋃ i, f' i = ⋃ i, Prod.mk a ⁻¹' f' i
h_disj : ∀ (a : β), Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i)
x : β
⊢ ((IsCondKernelCDF.toKernel f hf) (a, x)) (⋃ i, Prod.mk x ⁻¹' f' i) =
    ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' f' i)

Tactic:
rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]

Goal state after:
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 : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Tactic:
rw [setIntegral_compProd hs ht hf]

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 ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)

Tactic:
have : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t) := by
    congr; exact (ρ.disintegrate _).symm

Goal state after:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)
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 ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f ρ
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
  rw [← ρ.disintegrate ρ.condKernel] at hf
  rw [integral_compProd hf]

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 ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [setIntegral_compProd hs ht hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ (∀ᵐ (a : β) ∂Measure.map X μ, Integrable (fun ω ↦ f (a, ω)) ((Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a)) ∧
      Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a) (Measure.map X μ) ↔
    (∀ᵐ (a : β) ∂(Measure.map (fun a ↦ (X a, Y a)) μ).fst,
        Integrable (fun ω ↦ f (a, ω)) ((Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a)) ∧
      Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a)
        (Measure.map (fun a ↦ (X a, Y a)) μ).fst

Tactic:
Measure.fst_map_prodMk₀ hY

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ (∀ᵐ (a : β) ∂Measure.map X μ, Integrable (fun ω ↦ f (a, ω)) ((Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a)) ∧
      Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a) (Measure.map X μ) ↔
    (∀ᵐ (a : β) ∂Measure.map X μ, Integrable (fun ω ↦ f (a, ω)) ((Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a)) ∧
      Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a) (Measure.map X μ)
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ ⇑(μ ⊗ₘ κ).condKernel =ᵐ[μ] ⇑κ

Tactic:
suffices κ =ᵐ[(μ ⊗ₘ κ).fst] (μ ⊗ₘ κ).condKernel by symm; rwa [Measure.fst_compProd] at this

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ ⇑κ =ᵐ[(μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel
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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ ENNReal.ofReal (∫ (x : γ) in A, κ.density ν a x s ∂ν a) = (κ a) (A ×ˢ s)

pp: case hfi
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ Integrable (fun x ↦ κ.density ν a x s) ((ν a).restrict A)

pp: case f_nn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ 0 ≤ᵐ[(ν a).restrict A] fun x ↦ κ.density ν a x s

Tactic:
· rw [setIntegral_density hκν a hs hA, measureReal_def,
      ENNReal.ofReal_toReal (measure_ne_top _ _)]

Goal state after:
case hfi
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ Integrable (fun x ↦ κ.density ν a x s) ((ν a).restrict A)

case f_nn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ 0 ≤ᵐ[(ν a).restrict A] fun x ↦ κ.density ν a x s
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
this :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) {x | 1 ≤ κ.rnDerivAux (κ + η) a x} = 0
⊢ (η a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
withDensity_one_sub_rnDerivAux κ η

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
this : (η a) {x | 1 ≤ κ.rnDerivAux (κ + η) a x} = 0
⊢ (η a) (κ.mutuallySingularSetSlice η a) = 0
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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
⊢ f ⁻¹' ∅ = ∅

Tactic:
Set.preimage_empty

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e'_5
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
u_fin : Finite ↑u
x✝ : Fintype ↑u := Fintype.ofFinite ↑u
⊢ 0 = (Measure.pi fun i ↦ μ ↑i) (⋂ n, B n)

Tactic:
rw [B_inter, measure_empty]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e'_5
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
u_inf : Infinite ↑u
count_u : Countable ↑u
φ : ℕ ≃ ↑u
⊢ 0 = (Measure.map (⇑(piCongrLeft (fun i ↦ X ↑i) φ)) (infinitePiNat fun n ↦ μ ↑(φ n))) (⋂ n, B n)

Tactic:
rw [B_inter, measure_empty]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_f
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
i : ↥s
⊢ (μ ↑i) (if h : ↑i ∈ s then t ⟨↑i, h⟩ else Set.univ) = (μ ↑i) (t i)

Tactic:
rw [dif_pos i.2]

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 Ω
⊢ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ = ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ

Tactic:
compProd_posterior_eq_swap_comp

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ = ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ⇑Kernel.id =ᵐ[⇑Kernel.id ∘ₘ μ] ⇑(Kernel.id†μ)

Tactic:
refine ae_eq_posterior_of_compProd_eq_swap_comp Kernel.id ?_

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (⇑Kernel.id ∘ₘ μ) ⊗ₘ Kernel.id = ⇑(Kernel.swap Ω Ω) ∘ₘ μ ⊗ₘ Kernel.id
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) ∘ₘ μ =
    ⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) ∘ₘ μ

Tactic:
rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]

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))) ((↑s).pi t)

Tactic:
enter [2, 1]

Goal state after:
ι : 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)
| ↑s
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∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
f : 𝓧 → 𝓨
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hf : IsArgminEstimator ℓ P π f
hl : Measurable (Function.uncurry ℓ)
⊢ avgRisk ℓ P hf.kernel π ≤ bayesRisk ℓ P π

Tactic:
rw [hf.avgRisk_eq_lintegral_iInf hl]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
f : 𝓧 → 𝓨
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hf : IsArgminEstimator ℓ P π f
hl : Measurable (Function.uncurry ℓ)
⊢ ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π ≤ bayesRisk ℓ P π
Module: Mathlib.Probability.Distributions.Bernoulli

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Ber(x, y, p) s = if x ∈ s then if y ∈ s then 1 else ↑(toNNReal p) else if y ∈ s then ↑(toNNReal (σ p)) else 0

Tactic:
by
  split_ifs <;> simp_all [bernoulliMeasure_def, ← ENNReal.coe_add]

Goal state after:
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r x : ℝ
⊢ ENNReal.ofReal (exponentialPDFReal r x) = ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)

Tactic:
exponentialPDFReal,

Goal state after:
r x : ℝ
⊢ ENNReal.ofReal (gammaPDFReal 1 r x) = ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
p : PMF α
inst✝ : MeasurableSingletonClass α
s : Set α
⊢ p.toMeasure s = p.toOuterMeasure s

Tactic:
by
  have hs := (p.support_countable.mono s.inter_subset_right).measurableSet
  rw [← restrict_toMeasure_support, Measure.restrict_apply' p.support_countable.measurableSet,
    p.toMeasure_apply_eq_toOuterMeasure_apply hs, toOuterMeasure_apply_inter_support]

Goal state after:
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun a ↦ -rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1

Tactic:
exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
⊢ Measure.map f p.toMeasure = (map f p).toMeasure

Tactic:
ext s hs : 1

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f p.toMeasure) s = (map f p).toMeasure s
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
inst✝¹ : SFinite P
Y : Ω → 𝓨 × 𝓩
κ : Kernel 𝓧 (𝓨 × 𝓩)
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
⊢ HasCondDistrib (fun ω ↦ (Y ω).2) X κ.snd P

Tactic:
rw [Kernel.snd_eq]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
inst✝¹ : SFinite P
Y : Ω → 𝓨 × 𝓩
κ : Kernel 𝓧 (𝓨 × 𝓩)
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
⊢ HasCondDistrib (fun ω ↦ (Y ω).2) X (κ.map Prod.snd) P
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
⊢ Measure.map X ℙ = μ[|toMeasurable μ s] ↔ Measure.map X ℙ = μ[|s]

Tactic:
rw [ProbabilityTheory.cond_toMeasurable_eq]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this : IsProbabilityMeasure P
⊢ iIndepFun (fun p ω ↦ X p.fst p.snd ω) P

Tactic:
have : ∀ i j, IsProbabilityMeasure (P.map (X i j)) :=
    fun i j ↦ isProbabilityMeasure_map (mX i j).aemeasurable

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this✝ : IsProbabilityMeasure P
this : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (map (X i j) P)
⊢ iIndepFun (fun p ω ↦ X p.fst p.snd ω) P
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
mX : MeasurableSpace 𝓧
A : Set Ω
X : Ω → 𝓧
h : A.indicator 1 ⟂ᵢ[P] X
s : Set Ω
hs : s ∈ {A}
t : Set 𝓧
ht : MeasurableSet t
hA' : A = A.indicator 1 ⁻¹' {1}
⊢ P (A.indicator 1 ⁻¹' {1} ∩ X ⁻¹' t) = P (A.indicator 1 ⁻¹' {1}) * P (X ⁻¹' t)

Tactic:
exact h.measure_inter_preimage_eq_mul _ _ (by simp) ht

Goal state after: