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

Goal state before:
pp: α : 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 μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
a : α
⊢ κ a ⟂ₘ η a → (κ a) (Prod.mk a ⁻¹' s)ᶜ = 0

Tactic:
ha

Goal state after:
α : 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 μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
a : α
ha : κ a ⟂ₘ η a
⊢ (κ a) (Prod.mk a ⁻¹' s)ᶜ = 0
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
a : α
⊢ (κ.singularPart η) a = 0 → κ a ≪ η a

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
a : α
ha : (κ.singularPart η) a = 0
⊢ κ a ≪ η a
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
a : α
⊢ κ a ≪ η a → κ a = (η.withDensity (κ.rnDeriv η)) a

Tactic:
ha

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
a : α
ha : κ a ≪ η a
⊢ κ a = (η.withDensity (κ.rnDeriv η)) a
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
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)

Tactic:
apply tendsto_nhds_unique (f := fun s' : Finset s ↦ ∏ i ∈ s', μ i (t i)) (l := atTop)

Goal state after:
case ha
ι✝ : 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
⊢ Tendsto (fun s' ↦ ∏ i ∈ s', (μ ↑i) (t ↑i)) atTop (𝓝 ((infinitePi μ) (s.pi t)))

case hb
ι✝ : 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
⊢ Tendsto (fun s' ↦ ∏ i ∈ s', (μ ↑i) (t ↑i)) atTop (𝓝 (∏' (i : ↑s), (μ ↑i) (t ↑i)))
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†μ)
a : Ω
⊢ Kernel.id a = (Kernel.id†μ) a → (Kernel.id†μ) a = Kernel.id a

Tactic:
ha

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
this : ⇑Kernel.id =ᵐ[μ] ⇑(Kernel.id†μ)
a : Ω
ha : Kernel.id a = (Kernel.id†μ) a
⊢ (Kernel.id†μ) a = Kernel.id a
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    (⇑(Kernel.deterministic f hf) ∘ₘ μ) ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)

Tactic:
Measure.deterministic_comp_eq_map

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ = ⇑(Kernel.copy 𝓧) ∘ₘ Measure.map f μ

Tactic:
Measure.deterministic_comp_eq_map

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.copy 𝓧) ∘ₘ Measure.map f μ = ⇑(Kernel.copy 𝓧) ∘ₘ Measure.map f μ
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 ∂π ≤ (⨅ x, ∫⁻ (θ : Θ), ℓ θ x ∂π) * (⇑κ ∘ₘ μ) Set.univ

Tactic:
rw [Measure.comp_apply_univ, ENNReal.iInf_mul' hl_pos (fun hμ ↦ h_zero (by simpa using hμ))]

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 ∂π ≤ ⨅ i, (∫⁻ (θ : Θ), ℓ θ i ∂π) * μ Set.univ
Module: Mathlib.Probability.Decision.Risk.Countable

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Fintype 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
⊢ avgRisk ℓ P κ π = ∑ y, ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ P θ) {y} ∂π

Tactic:
avgRisk_countable' hℓ,

Goal state after:
Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Fintype 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
⊢ ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ P θ) {y} ∂π = ∑ y, ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ P θ) {y} ∂π
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂⇑(Kernel.boolKernel μ ν) ∘ₘ π,
    (((Kernel.boolKernel μ ν)†π) x) {false} = π {false} * (∂μ/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
by
  filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
  rw [hx]
  simp

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

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂⇑(Kernel.boolKernel μ ν) ∘ₘ π,
    (((Kernel.boolKernel μ ν)†π) x) {true} = π {true} * (∂ν/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
by
  filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
  rw [hx]
  simp

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

Goal state before:
pp: a r x : ℝ
hx : 0 ≤ x
⊢ gammaPDF a r x = ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))

Tactic:
by
  simp only [gammaPDF_eq, if_pos hx]

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

Goal state before:
pp: n : ℕ
p : ↑I
⊢ Bin(n, p).real {0} = (1 - ↑p) ^ n

Tactic:
by simp [binomial_real_singleton]

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

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n : ℕ
p : ↑I
⊢ Bin(R, n, p).real {0} = (1 - ↑p) ^ n

Tactic:
← Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n : ℕ
p : ↑I
⊢ Bin(R, n, p).real {↑0} = (1 - ↑p) ^ n
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
⊢ Bin(n, p).real {n} = ↑p ^ n

Tactic:
by simp [binomial_real_singleton]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
a : ℝ
⊢ a ∈ Icc 0 x →
    (fun x ↦ ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)) a =
      (fun x ↦ ENNReal.ofReal (r * rexp (-(r * x)))) a

Tactic:
ha

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
a : ℝ
ha : a ∈ Icc 0 x
⊢ (fun x ↦ ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)) a =
    (fun x ↦ ENNReal.ofReal (r * rexp (-(r * x)))) a
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
mR : MeasurableSpace R
inst✝ : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
⊢ Po(R, r₁) ∗ Po(R, r₂) = Po(R, r₁ + r₂)

Tactic:
by
  rw [← Nat.coe_castAddMonoidHom, ← Measure.map_conv_addMonoidHom _ (by fun_prop),
    poissonMeasure_conv_poissonMeasure]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
r₁ r₂ : ℝ≥0
X Y : Ω → ℕ
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(r₁) P
hY : HasLaw Y Po(r₂) P
⊢ HasLaw (X + Y) (Po(r₁) ∗ Po(r₂)) P

Tactic:
exact hXY.hasLaw_add hX hY

Goal state after:
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₁) ∗ Po(R, r₂)) P

Tactic:
exact hXY.hasLaw_add hX hY

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
⊢ (κ a) (t ∩ t) = (κ a) t * (κ a) t → (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
a : α
⊢ IsProbabilityMeasure (κ a) → IsFiniteMeasure (κ a)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure (κ a)
⊢ IsFiniteMeasure (κ a)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
a : α
⊢ IsProbabilityMeasure (κ a) → IsFiniteMeasure (κ a)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure (κ a)
⊢ IsFiniteMeasure (κ a)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
a : α
⊢ IsProbabilityMeasure (κ a) → IsFiniteMeasure (κ a)

Tactic:
ha

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure (κ a)
⊢ IsFiniteMeasure (κ a)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.copy (X.carrier × Y.carrier) =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              (Kernel.id ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯) ∘ₖ
            (Kernel.id ∥ₖ (Kernel.swap X.carrier Y.carrier ∥ₖ Kernel.id)) ∘ₖ
          (Kernel.id ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.id ∥ₖ Kernel.copy Y.carrier ∘ₖ (Kernel.copy X.carrier ∥ₖ Kernel.id))

Tactic:
simp only [Kernel.copy, Kernel.id, Kernel.swap]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯) ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
⊢ μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] stoppedValue f τ

Tactic:
ae_eq_restrict_iff_indicator_ae_eq
    (hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ))

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
⊢ {ω | τ ω ≤ σ ω}.indicator μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ] {ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
⊢ ∀ x₁ ∈ ρ₁.toSubmodule, ∀ x₂ ∈ ρ₂.toSubmodule, (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
x₁

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
⊢ x₁ ∈ ρ₁.toSubmodule → ∀ x₂ ∈ ρ₂.toSubmodule, (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
⊢ ∀ (g : G) ⦃v : W⦄, v ∈ ρ₁.toSubmodule ⊓ ρ₂.toSubmodule → (ρ g) v ∈ ρ₁.toSubmodule ⊓ ρ₂.toSubmodule

Tactic:
simp only [Submodule.mem_inf, and_imp]

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
⊢ ∀ (g : G) ⦃v : W⦄, v ∈ ρ₁.toSubmodule → v ∈ ρ₂.toSubmodule → (ρ g) v ∈ ρ₁.toSubmodule ∧ (ρ g) v ∈ ρ₂.toSubmodule
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
z : A[G]
hz : z ∈ Submonoid.center A[G]
x✝ : G
⊢ ρ.asAlgebraHom z ∘ₗ ρ x✝ = ρ x✝ ∘ₗ ρ.asAlgebraHom z

Tactic:
← ρ.asAlgebraHom_of,

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
z : A[G]
hz : z ∈ Submonoid.center A[G]
x✝ : G
⊢ ρ.asAlgebraHom z ∘ₗ ρ.asAlgebraHom ((MonoidAlgebra.of A G) x✝) =
    ρ.asAlgebraHom ((MonoidAlgebra.of A G) x✝) ∘ₗ ρ.asAlgebraHom z
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat k[G]
⊢ ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M

Tactic:
dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
  exact (Representation.ofModule M).asModuleEquiv.toAddEquiv.trans
    (RestrictScalars.addEquiv k k[G] _)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
let φ : ℕ → SimpleFunc E E :=
    SimpleFunc.nearestPt (fun k => Nat.casesOn k 0 ((↑) ∘ denseSeq s) : ℕ → E)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))