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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)

Tactic:
refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (fun x ↦ (X x, (f ∘ Y) x)) μ = Measure.map X μ ⊗ₘ (condDistrib Y X μ).map f
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)

Tactic:
refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (fun x ↦ (X x, (f ∘ X) x)) μ = Measure.map X μ ⊗ₘ Kernel.deterministic f hf
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
m n : ι
⊢ Measurable (IicProdIoc m n)

Tactic:
by
  refine measurable_pi_lambda _ (fun i ↦ ?_)
  by_cases h : i ≤ m
  · simpa [IicProdIoc, h] using measurable_fst.eval
  · simpa [IicProdIoc, h] using measurable_snd.eval

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

Goal state before:
pp: case iUnion
α : 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 γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), ∫ (x : γ) in f i, κ.density ν a x s ∂ν a = (κ a).real (f i ×ˢ s)
⊢ ∑' (n : ℕ), ∫ (x : γ) in f n, κ.density ν a x s ∂ν a = (κ a).real ((⋃ i, f i) ×ˢ s)

Tactic:
simp_rw [h_eq, measureReal_def]

Goal state after:
case iUnion
α : 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 γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), ∫ (x : γ) in f i, κ.density ν a x s ∂ν a = (κ a).real (f i ×ˢ s)
⊢ ∑' (n : ℕ), ((κ a) (f n ×ˢ s)).toReal = ((κ a) ((⋃ i, f i) ×ˢ s)).toReal
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab : a ≤ b
k : ℕ
h : b ≤ k
hk : partialTraj κ b k ∘ₖ partialTraj κ a b = partialTraj κ a k
⊢ partialTraj κ k (k + 1) ∘ₖ (partialTraj κ b k ∘ₖ partialTraj κ a b) = partialTraj κ a (k + 1)

Tactic:
hk,

Goal state after:
case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab : a ≤ b
k : ℕ
h : b ≤ k
hk : partialTraj κ b k ∘ₖ partialTraj κ a b = partialTraj κ a k
⊢ partialTraj κ k (k + 1) ∘ₖ partialTraj κ a k = partialTraj κ a (k + 1)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ partialTraj κ k k.succ ∘ₖ partialTraj κ a k =
    (Kernel.id ×ₖ (partialTraj κ a (k + 1)).map (restrict₂ ⋯)).map (_root_.IicProdIoc a (k + 1))

Tactic:
hk,

Goal state after:
case inr.succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ partialTraj κ k k.succ ∘ₖ (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k) =
    (Kernel.id ×ₖ (partialTraj κ a (k + 1)).map (restrict₂ ⋯)).map (_root_.IicProdIoc a (k + 1))
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} =
    (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) (cylinder {i} {fun x ↦ True})

Tactic:
setBernoulli_apply'

Goal state after:
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) ((fun p ↦ {i | p i}) ⁻¹' {s | i ∈ s}) =
    (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) (cylinder {i} {fun x ↦ True})
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)
⊢ IsProjectiveMeasureFamily fun I ↦ Measure.pi fun i ↦ μ ↑i

Tactic:
by
  refine fun I J hJI ↦ Measure.pi_eq (fun s ms ↦ ?_)
  classical
  simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
  refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
  · rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
⊢ Var[0; μ | m] = 0

Tactic:
by simp [condVar]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)

Tactic:
· exact ⟨⟨B * κ.bound, ENNReal.mul_lt_top hB_top.lt_top κ.bound_lt_top, fun a => by
        rw [Kernel.withDensity_apply' κ hf a Set.univ]
        calc
          ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
          _ = B * κ a Set.univ := by
            simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
          _ ≤ B * κ.bound := by grw [measure_le_bound]⟩⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)
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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
x y : (i : ℕ) → X i
n i : ℕ
hi : i ∈ ↑(Iic p)
⊢ updateFinset x (Iic p) x₀ i = updateFinset y (Iic p) x₀ i

Tactic:
mem_coe,

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)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
x y : (i : ℕ) → X i
n i : ℕ
hi : i ∈ Iic p
⊢ updateFinset x (Iic p) x₀ i = updateFinset y (Iic p) x₀ i
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 : α
s : Set γ
hs : MeasurableSet s
⊢ ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a)
      (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)

Tactic:
simp only [FunLike.coe_add, Pi.add_apply, Measure.coe_add]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) +
      ((κ.singularPart η) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) univ + ((κ.singularPart η) a) univ = (κ a) univ

Tactic:
conv_rhs => rw [← rnDeriv_add_singularPart κ η]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) univ + ((κ.singularPart η) a) univ =
    ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) univ
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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
l : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
hl : ∀ (k : ℕ) (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = ε
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → ((i : ↥(Iic k)) → X ↑i) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X ↑i),
    (∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) y)) →
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (χ n) (update (updateFinset x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction x₀ ind
main :
  ∀ (k : ℕ),
    p ≤ k →
      ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) (frestrictLe k z))
aux :
  ∀ (x : (i : ℕ) → X i) (n : ℕ),
    (trajContent κ x₀) (A n) = lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)
this✝ : 0 ≠ ε
n : ℕ
this : 0 < χ n z
⊢ z ∈ A n

Tactic:
exact Set.mem_of_indicator_ne_zero (ne_of_lt this).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
⊢ ∀ᵐ (x : α × β) ∂μ ⊗ₘ η, κ.rnDeriv η x.1 x.2 = 1

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (by fun_prop) fun s hs _ ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
s : Set (α × β)
hs : MeasurableSet s
x✝ : (μ ⊗ₘ η) s < ∞
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = ∫⁻ (x : α × β) in s, 1 ∂μ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝ : ∀ (a : α), IsZeroOneMeasure (κ a)
⊢ IsDeterministic κ

Tactic:
refine ⟨?_⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝ : ∀ (a : α), IsZeroOneMeasure (κ a)
⊢ κ ∥ₖ κ ∘ₖ copy α = copy β ∘ₖ κ
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
s' : Finset ↑s
| (infinitePi fun i ↦ μ ↑i) ((↑s').pi fun i ↦ t ↑i)

Tactic:
← infinitePi_map_restrict',

Goal state after:
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
s' : Finset ↑s
| (map s.domRestrict (infinitePi μ)) ((↑s').pi fun i ↦ t ↑i)
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)
| ↑s

Tactic:
rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]

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)
| ⇑e '' ↑(s.preimage ⇑e ⋯)
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∞
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, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π ≤ avgRisk ℓ (Kernel.const Θ μ) κ π

Tactic:
rw [avgRisk_const_left' hl]

Goal state after:
Θ : 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, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π ≤ ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂⇑κ ∘ₘ μ
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∞
inst✝² : Nonempty 𝓨
P : Kernel Θ 𝓧
inst✝¹ : IsFiniteKernel P
π : Measure Θ
inst✝ : IsFiniteMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ bayesRisk ℓ P π < ∞

Tactic:
refine (bayesRisk_le_mul' P π hℓC).trans_lt ?_

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝² : Nonempty 𝓨
P : Kernel Θ 𝓧
inst✝¹ : IsFiniteKernel P
π : Measure Θ
inst✝ : IsFiniteMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ↑C * P.bound * π Set.univ < ∞
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 π
⊢ ⇑(Kernel.id ∥ₖ κ) ∘ₘ π ⊗ₘ P = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(P†π ×ₖ Kernel.id) ∘ₘ ⇑P ∘ₘ π

Tactic:
by rw [posterior_prod_id_comp]

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

Goal state before:
pp: x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (y : ℝ) in Iio x, gammaPDF a r y = 0

Tactic:
by
  rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
  · rw [lintegral_zero, ← ENNReal.ofReal_zero]
  · intro a (_ : a < _)
    simp only [gammaPDF_eq, ENNReal.ofReal_eq_zero]
    rw [if_neg (by linarith)]

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

Goal state before:
pp: r x : ℝ
⊢ HasDerivAt (fun a ↦ -rexp (-(r * a))) (r * rexp (-(r * x))) x

Tactic:
convert! (((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1)) using 1

Goal state after:
case e'_8
r x : ℝ
⊢ (fun a ↦ -rexp (-(r * a))) = fun y ↦ -1 * rexp (-r * id y)

case e'_9
r x : ℝ
⊢ r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < paretoPDFReal t r x

Tactic:
rw [paretoPDFReal, if_pos hx]
  have _ : 0 < x := by linarith
  positivity

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

Goal state before:
pp: case refine_2
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
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) ((traj κ a) x₀)

Tactic:
· exact (i_f'.1.comp_ae_measurable' (measurable_frestrictLe b).aemeasurable)

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = if a ∈ s then 1 else 0

Tactic:
split_ifs with ha

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 1

case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r₁ r₂ : ℝ≥0
t : ℝ
⊢ charFun (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) t = charFun Po(ℝ, r₁ + r₂) t

Tactic:
simp only [charFun_conv, charFun_map_cast_poissonMeasure, ← Complex.exp_add]

Goal state after:
r₁ r₂ : ℝ≥0
t : ℝ
⊢ Complex.exp (↑↑r₁ * (Complex.exp (↑t * Complex.I) - 1) + ↑↑r₂ * (Complex.exp (↑t * Complex.I) - 1)) =
    Complex.exp (↑↑(r₁ + r₂) * (Complex.exp (↑t * Complex.I) - 1))
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
mR : MeasurableSpace R
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
X Y : Ω → R
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(R, r₁) P
hY : HasLaw Y Po(R, r₂) P
⊢ HasLaw (X + Y) Po(R, r₁ + r₂) P

Tactic:
← map_cast_poissonMeasure_conv

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
mR : MeasurableSpace R
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
X Y : Ω → R
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(R, r₁) P
hY : HasLaw Y Po(R, r₂) P
⊢ HasLaw (X + Y) (Po(R, r₁) ∗ Po(R, r₂)) P
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

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

Tactic:
intro h'
      simp only [tsub_eq_zero_iff_le, one_le_coe_iff] at h'
      exact eq_of_le_of_ge h h'

Goal state after: