mathlib-initiative/mathlib-tactics huggingface dataset:
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)
ν : 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)
⊢ (map s.restrict ν) (Set.univ.pi t) = ∏ i, (μ ↑i) (t i)

Tactic:
Measure.map_apply,

Goal state after:
ι : 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)
⊢ ν (s.restrict ⁻¹' Set.univ.pi t) = ∏ i, (μ ↑i) (t i)

case hf
ι : 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)
⊢ Measurable s.restrict

case hs
ι : 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)
⊢ MeasurableSet (Set.univ.pi t)
Module: Mathlib.Probability.Kernel.CompProdEqIff

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
s : Set (α × β)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (a_1 : β), (Prod.mk a ⁻¹' s).indicator (f a) a_1 ∂κ a = ∫⁻ (b : β), s.indicator (fun a ↦ f a.1 a.2) (a, b) ∂κ a

Tactic:
rfl

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)
ι : 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.pi t = s.pi fun i ↦ if i ∈ s then t i else Set.univ

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case a
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
Y : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this✝ : ∀ (i : ι), IsProbabilityMeasure (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (fun x i ↦ f i (x i)) ⁻¹' (↑s).pi t = (↑s).pi fun i ↦ f i ⁻¹' t i
i : ι
hi : i ∈ s
⊢ (μ i) (f i ⁻¹' t i) = (map (f i) (μ i)) (t i)

Tactic:
rw [map_apply (by fun_prop) (ht i)]

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 Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
x : 𝓧
h_ac' : (κ†μ) x ≪ μ
⊢ ∫⁻ (ω : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂(Kernel.const 𝓧 μ) x = ((κ†μ) x) s

Tactic:
Kernel.setLIntegral_rnDeriv h_ac' hs

Goal state after:
Ω : 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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
x : 𝓧
h_ac' : (κ†μ) x ≪ μ
⊢ ((κ†μ) x) s = ((κ†μ) x) s
Module: Mathlib.Probability.ProductMeasure

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

Tactic:
· exact .pi ((countable_toSet _).image e) (by simp_all)

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
π : Measure Θ
inst✝ : SFinite π
⊢ bayesRisk ℓ (Kernel.discard Θ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π

Tactic:
by
  rw [Kernel.discard_eq_const, bayesRisk_const hl]

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
e : { κ // IsMarkovKernel κ } ≃ { μ // IsProbabilityMeasure μ } :=
  { toFun := fun κ ↦ ⟨↑κ x, ⋯⟩, invFun := fun μ ↦ ⟨Kernel.const 𝓧 ↑μ, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ ⨅ x, avgRisk ℓ P (↑(e.symm x)) π = ⨅ x, avgRisk ℓ P (Kernel.const 𝓧 ↑x) π

Tactic:
rfl

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)
inst✝ : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → ℝ≥0∞ := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ (∫⁻ (y : (i : ↥s) → X ↑i), g y ∂Measure.pi fun i ↦ μ ↑i) = (∫⋯∫⁻_s, f ∂μ) x

Tactic:
rfl

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 Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
x : 𝓧
h✝ : ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_ac' : (κ†μ) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_eq : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = (∂(κ†μ) x/∂(Kernel.const 𝓧 μ) x) ω
⊢ ω ∈ s → (∂(κ†μ) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x

Tactic:
hωs

Goal state after:
Ω : 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 : 𝓧
h✝ : ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_ac' : (κ†μ) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_eq : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = (∂(κ†μ) x/∂(Kernel.const 𝓧 μ) x) ω
hωs : ω ∈ s
⊢ (∂(κ†μ) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
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✝¹ : Countable 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
⊢ ∑' (i : 𝓨), ∫⁻ (a : Θ), ℓ a i * ((κ ∘ₖ P) a) {i} ∂π = ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ P θ) {y} ∂π

Tactic:
rfl

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ ((partialTraj κ a b) u ⊗ₘ traj κ b) s = (Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) u)) s

Tactic:
Measure.map_apply,

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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ ((partialTraj κ a b) u ⊗ₘ traj κ b) s = ((traj κ a) u) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, x)

case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ (Measure.map (fun x_1 ↦ updateFinset x_1 (Iic b) x) ((traj κ b) x)) (Prod.mk x ⁻¹' s) =
    (Measure.map (fun x_1 ↦ updateFinset x_1 (Iic b) x) ((traj κ b) x)) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

Tactic:
Measure.map_apply,

Goal state after:
case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) =
    (Measure.map (fun x_1 ↦ updateFinset x_1 (Iic b) x) ((traj κ b) x)) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

case e_f.hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ Measurable fun x_1 ↦ updateFinset x_1 (Iic b) x

case e_f.hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet (Prod.mk x ⁻¹' s)
Module: Mathlib.Probability.Distributions.Cauchy

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

Tactic:
rfl

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ cauchyPDF x₀ γ x = ENNReal.ofReal (cauchyPDFReal x₀ γ x)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
p : ↑I
k : ℕ
⊢ 0 ≤ ↑p

Tactic:
grind

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

Goal state before:
pp: n : ℕ
p : ↑I
k : ℕ
⊢ 0 ≤ 1 - ↑p

Tactic:
grind

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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (n : ℕ) → X n), (frestrictLe b ⁻¹' A).indicator ((fun x_1 ↦ f x_1 x) ∘ frestrictLe b) x ∂(traj κ a) u =
    ∫ (x : (i : ℕ) → X i), (frestrictLe b ⁻¹' A).indicator (fun y ↦ f (frestrictLe b y) y) x ∂(traj κ a) u

Tactic:
rfl

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
x✝ : a ≤ x
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = 0

Tactic:
if_neg (by linarith),

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
x✝ : a ≤ x
⊢ ENNReal.ofReal 0 = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (⇑μ.toPMF) x = ∑' (x : α), s.indicator (fun x ↦ μ {x}) x

Tactic:
rfl

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

Goal state before:
pp: p : ↑unitInterval
n : ℕ
⊢ 0 ≤ 1 - ↑p

Tactic:
grind

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

Goal state before:
pp: p : ↑unitInterval
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < 1 - ↑p

Tactic:
grind

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

Goal state before:
pp: p : ↑unitInterval
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < ↑p

Tactic:
grind

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

Goal state before:
pp: p : ↑unitInterval
hp : p ≠ 0
⊢ 0 ≤ 1 - ↑p

Tactic:
grind

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

Goal state before:
pp: p : ↑unitInterval
hp : p ≠ 0
⊢ 1 - ↑p < 1

Tactic:
grind

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

Goal state before:
pp: case e'_6
p : ↑unitInterval
hp : p ≠ 0
⊢ 1 = (1 - (1 - ↑p))⁻¹ * ↑p

Tactic:
grind

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

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
n : ℕ
hn : k ≤ n
hne : p n < 1 / 2
⊢ 1 - p n ≠ 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = s.indicator 1 a

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∈ s
⊢ (f a) b = (f a) b

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∉ s
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
⊢ (∑' (a : α), if f a ∈ s then p a else 0) = ∑' (x : α), if x ∈ f ⁻¹' s then p x else 0

Tactic:
rfl

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal (poissonPMFReal r n) = ⟨fun n ↦ ENNReal.ofReal (poissonPMFReal r n), ⋯⟩ n

Tactic:
rfl

Goal state after:
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 Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
⊢ Measure.map (fun a ↦ ((f ∘ Z) a, Y a)) P = Measure.map (Prod.map f id ∘ fun a ↦ (Z a, Y a)) P

Tactic:
rfl

Goal state after:
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 Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
s : Set (𝓧 × 𝓨)
hs : MeasurableSet s
⊢ ∫⁻ (a : 𝓩), ((κ.comap f hf) a) (Prod.mk a ⁻¹' Prod.map f id ⁻¹' s) ∂Measure.map Z P =
    ∫⁻ (a : 𝓩), (κ (f a)) (Prod.mk (f a) ⁻¹' s) ∂Measure.map Z P

Tactic:
rfl

Goal state after:
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 : Ω → 𝓧
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝² : SFinite P
inst✝¹ : IsSFiniteKernel κ
Z : Ω → 𝓩
η : Kernel (𝓧 × 𝓨) 𝓩
inst✝ : IsMarkovKernel η
h : HasCondDistrib (fun a ↦ (Y a, Z a)) X (κ ⊗ₖ η) P
hZ : AEMeasurable Z P
hY : AEMeasurable Y P
⊢ Measure.map (fun a ↦ ((X a, Y a), Z a)) P =
    Measure.map (⇑MeasurableEquiv.prodAssoc.symm ∘ fun ω ↦ (X ω, (fun a ↦ (Y a, Z a)) ω)) P

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
i : ι
⊢ map (X i ∘ fun x ↦ x i) (infinitePi P) = map (fun ω ↦ X i (ω i)) (infinitePi P)

Tactic:
Function.comp_def

Goal state after:
ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
i : ι
⊢ map (fun x ↦ X i (x i)) (infinitePi P) = map (fun ω ↦ X i (ω i)) (infinitePi P)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ (↑s.card)⁻¹ * ↑s.card = 1

Tactic:
ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1))
              (ENNReal.natCast_ne_top _)

Goal state after:
α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ 1 = 1
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (ω : Ω) ∂⇑(condExpKernel μ m) ∘ₘ μ.trim hm, f ω = AEStronglyMeasurable.mk f hf ω

Tactic:
condExpKernel_comp_trim hm

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = AEStronglyMeasurable.mk f hf ω
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case pos
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : μ s = 0
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᵐ[0] fun x ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
rfl

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
have : (fun ω ↦ (condExpKernel μ (generateFrom {s}) ω).real t) =ᵐ[μ.restrict s]
      μ⟦t | generateFrom {s}⟧ :=
    ae_restrict_le <| condExpKernel_ae_eq_condExp
      (generateFrom_singleton_le hs) ht

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑prodAssoc.symm ∘ ⇑prodAssoc) ⋯ = Kernel.deterministic id ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑prodAssoc ∘ ⇑prodAssoc.symm) ⋯ = Kernel.deterministic id ⋯

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X), B.indicator (fun a ↦ (π a) A) a ∂μ = ∫⁻ (a : X), B.indicator (fun x ↦ (π a) A) a ∂μ

Tactic:
rfl

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

Goal state before:
pp: case mpr
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']) →
    ∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i = s i) →
        μ[(⋂ i ∈ s_1, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ x ∈ s_1, μ[(s x).indicator fun ω ↦ 1 | m']

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case e_f
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
a : Y₁✝.carrier
⊢ ∫⁻ (y : Y₂✝.carrier), (η.hom a✝.2) (Prod.mk (a, y) ⁻¹' ⇑prodAssoc ⁻¹' s✝) ∂κ₂.hom a✝.1.2 =
    ∫⁻ (x : Y₂✝.carrier), (η.hom (prodAssoc a✝).2.2) (Prod.mk x ⁻¹' Prod.mk a ⁻¹' s✝) ∂κ₂.hom (prodAssoc a✝).2.1

Tactic:
rfl

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) →
        μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (f i)) →
        μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ (κ.hom a✝.2) (Prod.mk a✝.1 ⁻¹' Prod.snd ⁻¹' s✝) = (κ.hom a✝.2) s✝

Tactic:
rfl

Goal state after: