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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ (κ a).real (A ×ˢ Iic ↑↑r)

Tactic:
← hf.setIntegral a hA

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ∫ (c : β) in A, f (a, c) ↑r ∂ν a
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ (κ a).real (A ×ˢ Iic ↑q) ≤ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a

Tactic:
← hf.setIntegral a hA

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∫ (c : β) in A, f (a, c) q ∂ν a ≤ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a
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
hρ : ρ ≠ 0
⊢ IsSFiniteKernel ρCond

Tactic:
contrapose hρ; rwa [← ρ.disintegrate ρCond, Measure.compProd_of_not_isSFiniteKernel]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
| (κ.fst a) s

Tactic:
rw [← h]

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
| ((κ.fst ⊗ₖ κCond).fst a) s
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
u : ↑↑S
⊢ ∫ (x : γ) in ↑u, κ.densityProcess ν n a x s ∂ν a = ((κ a) (↑u ×ˢ s)).toReal

Tactic:
rw [setIntegral_densityProcess_of_mem hκν _ _ hs (hS_subset (by simp))]

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
u : ↑↑S
⊢ (κ a).real (↑u ×ˢ s) = ((κ a) (↑u ×ˢ s)).toReal
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 i : ι
hi : i ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }
      c i

Tactic:
simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]

Goal state after:
case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : i ≤ a
⊢ Measurable fun c ↦ c.1 ⟨i, ⋯⟩
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 i : ι
hi : ¬i ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }
      c i

Tactic:
simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]

Goal state after:
case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : ¬i ≤ a
⊢ Measurable fun c ↦ c.2 ⟨i, ⋯⟩
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᵐ[μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | ?m.39] ω = μ[Y | ?m.39] ω
⊢ (X ω - μ[X | m] ω) ^ 2 = (Y ω - μ[Y | m] ω) ^ 2

Tactic:
hω,

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᵐ[μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | ?m.39] ω = μ[Y | ?m.39] ω
⊢ (Y ω - μ[X | m] ω) ^ 2 = (Y ω - μ[Y | m] ω) ^ 2
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
⊢ (κ.withDensity f) a ≪ κ a

Tactic:
by_cases hf : Measurable (Function.uncurry f)
  · rw [Kernel.withDensity_apply _ hf]
    exact withDensity_absolutelyContinuous _ _
  · rw [withDensity_of_not_measurable _ hf]
    simp [Measure.AbsolutelyContinuous.zero]

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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (infinitePiNat fun n ↦ μ (e n)) (⇑(piCongrLeft X e) ⁻¹' I.restrict ⁻¹' S) = (piContent μ) (I.restrict ⁻¹' S)

pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)

Tactic:
← Set.preimage_comp,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (infinitePiNat fun n ↦ μ (e n)) (I.restrict ∘ ⇑(piCongrLeft X e) ⁻¹' S) = (piContent μ) (I.restrict ⁻¹' S)

ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)
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 η
h_le : κ ≤ κ + η
⊢ (((κ + η).withDensity fun a x ↦ ENNReal.ofReal 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun a x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η

Tactic:
ENNReal.ofReal_one

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
⊢ (((κ + η).withDensity fun a x ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun a x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a 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)
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
n : ℕ
⊢ f ⁻¹' (s n).restrict ⁻¹' S n = (t n).restrict ⁻¹' T n

Tactic:
← Set.preimage_comp,

Goal state after:
ι : 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
n : ℕ
⊢ (s n).restrict ∘ f ⁻¹' S n = (t n).restrict ⁻¹' T n
Module: Mathlib.Probability.Kernel.RadonNikodym

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

pp: case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0

Tactic:
· rw [h, zero_add]
    exact mutuallySingular_singularPart _ _ _

Goal state after:
case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0
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 : α
h_eq_add :
  ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) =
    (κ a) (κ.mutuallySingularSetSlice η a)
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
simp only [FunLike.coe_add, Pi.add_apply, Measure.coe_add,
    withDensity_rnDeriv_mutuallySingularSetSlice κ η, zero_add] at h_eq_add

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = (κ a) (κ.mutuallySingularSetSlice η a)
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
ι : 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
⊢ Tendsto (fun n ↦ (piContent fun i ↦ μ ↑i) (B n)) atTop (𝓝 0)

Tactic:
· -- If `u` is infinite, then we have an equivalence with `ℕ` so we can apply `secondLemma`.
    have count_u : Countable u := Set.countable_iUnion (fun n ↦ (s n).countable_toSet)
    obtain ⟨φ, -⟩ := Classical.exists_true_of_nonempty (α := ℕ ≃ u) nonempty_equiv_of_countable
    conv => enter [1]; ext n; rw [← infinitePiNat_map_piCongrLeft _ φ (B_mem n)]
    convert!
      tendsto_measure_iInter_atTop (fun n ↦ (mB n).nullMeasurableSet) B_anti ⟨0, measure_ne_top _ _⟩
    · rw [B_inter, measure_empty]
    · infer_instance

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)
s : Finset ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this : (↑s).pi t = cylinder s (Set.univ.pi fun i ↦ t ↑i)
⊢ ∏ i ∈ s.attach, (μ ↑i) (t ↑i) = ∏ i ∈ s, (μ i) (t i)

Tactic:
prod_attach _ (fun i ↦ (μ i) (t i))

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this : (↑s).pi t = cylinder s (Set.univ.pi fun i ↦ t ↑i)
⊢ ∏ x ∈ s, (μ x) (t x) = ∏ i ∈ s, (μ 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)
s : Finset ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
⊢ (infinitePi μ) ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)

Tactic:
by
  have : Set.pi s t = cylinder s ((@Set.univ s).pi (fun i : s ↦ t i)) := by
    ext x
    simp
  rw [this, cylinder, ← map_apply, infinitePi_map_restrict, pi_pi]
  · rw [univ_eq_attach, prod_attach _ (fun i ↦ (μ i) (t i))]
  · exact measurable_restrict _
  · exact .univ_pi fun i ↦ mt i.1 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:
by rw [compProd_posterior_eq_swap_comp]

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

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

Tactic:
by
    rw [Measure.id_comp] at this
    filter_upwards [this] with a ha using ha.symm

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
| frestrictLe b ∘ ⇑(IicProdIoi a)

Tactic:
change (IicProdIoc a b) ∘
    (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).1⟩))

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 b : ℕ
hb : b ≥ a + 1
| _root_.IicProdIoc a b ∘ Prod.map id fun x i ↦ x ⟨↑i, ⋯⟩
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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x

Tactic:
by
  convert!
    Measure.ae_ae_of_ae_prod
      (rnDeriv_posterior_ae_prod h_ac)

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

Tactic:
by
  refine le_antisymm ?_ (bayesRisk_le_avgRisk _ _ _ _)
  rw [hf.avgRisk_eq_lintegral_iInf hl]
  exact lintegral_iInf_posterior_le_bayesRisk hl _ _

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

Goal state before:
pp: α β : ℝ
⊢ ∫⁻ (x : ℝ) in Iio 1, betaPDF α β x ∂volume.restrict (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Tactic:
Measure.restrict_restrict measurableSet_Iio,

Goal state after:
α β : ℝ
⊢ ∫⁻ (x : ℝ) in Iio 1 ∩ Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
x : ℝ
⊢ 0 < π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹

Tactic:
positivity

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

Goal state before:
pp: x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
⊢ 0 < r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity

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

Goal state before:
pp: case pos
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
h✝ : 0 ≤ x
⊢ 0 ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
p : ↑I
k : ℕ
⊢ 0 ≤ ↑(n.choose k)

Tactic:
positivity

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

Goal state before:
pp: case neg
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
h✝ : ¬0 ≤ x
⊢ 0 ≤ 0

Tactic:
positivity

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ AEStronglyMeasurable (fun x ↦ r * rexp (-(r * x))) (volume.restrict (Icc 0 x))

r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
x : ℝ
hx : 0 ≤ x
⊢ 0 x ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity

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

Goal state before:
pp: p : ↑unitInterval
hp : p ≠ 0
n : ℕ
⊢ (Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n) {n} = ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)

Tactic:
Measure.sum_smul_dirac_singleton

Goal state after:
p : ↑unitInterval
hp : p ≠ 0
n : ℕ
⊢ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) = ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
x✝ : 0 < x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity

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

Goal state before:
pp: case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity

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

Goal state before:
pp: case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0

Tactic:
positivity

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

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < geometricPMFReal p n

Tactic:
rw [geometricPMFReal]
  positivity [sub_pos.mpr hp_lt_one]

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]

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)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
⊢ IsProbabilityMeasure (⇑(traj κ 0) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ (Measure.sum fun n ↦ ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !) • Measure.dirac n) {n} =
    ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)

Tactic:
Measure.sum_smul_dirac_singleton

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !) = ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ 0 ≤ rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
positivity

Goal state after: