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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ ρ'.fst s = ρ.fst s

Tactic:
hρ'def,

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ (Measure.map (Prod.map id f) ρ).fst s = ρ.fst s
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
s : Set (α × ℝ)
hs : MeasurableSet s
| ρ' s

Tactic:
hρ'def,

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
s : Set (α × ℝ)
hs : MeasurableSet s
| (Measure.map (Prod.map id f) ρ) s
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ ρ.condKernel a = (const Unit ρ).condKernelUnitBorel ((), a)

Tactic:
Measure.condKernel

Goal state after:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ ((const Unit ρ).condKernelUnitBorel.comap (fun a ↦ ((), a)) ⋯) a = (const Unit ρ).condKernelUnitBorel ((), a)
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ✝ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ✝
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
⊢ IsMarkovKernel ρ.condKernel

Tactic:
Measure.condKernel

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ✝ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ✝
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
⊢ IsMarkovKernel ((const Unit ρ).condKernelUnitBorel.comap (fun a ↦ ((), a)) ⋯)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : (fun x ↦ c) = (fun x ↦ c) ∘ X
b : β
hb : (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b
⊢ (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b

Tactic:
rw [hb]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)
⊢ Tendsto (fun m ↦ (κ a) (univ ×ˢ seq m)) atTop (𝓝 ((κ a) univ))

Tactic:
convert! tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)
⊢ univ = ⋃ n, univ ×ˢ seq n
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density ν a a_1 (seq i) ∂ν a) atTop (𝓝 0)

Tactic:
exact tendsto_integral_density_of_antitone hκν a seq hseq hseq_iInter hseq_meas

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 → (κ.fst a) (countablePartitionSet n x) ≠ 0) ∧
    ((κ a) (countablePartitionSet n x ×ˢ univ) = ∞ → (κ.fst a) (countablePartitionSet n x) = ∞)

Tactic:
simp_rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 → (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0) ∧
    ((κ a) (countablePartitionSet n x ×ˢ univ) = ∞ → (κ a) {p | p.1 ∈ countablePartitionSet n x} = ∞)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m)) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ)))

Tactic:
convert! tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ countablePartitionSet n x ×ˢ univ = ⋃ n_1, countablePartitionSet n x ×ˢ seq n_1
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ setBer(u, p).real {t | t ⊆ u ∧ t.ncard ∈ {k}} = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
← Set.biUnion_of_singleton (Set.ofPred _)

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ setBer(u, p).real (⋃ x ∈ {t | t ⊆ u ∧ t.ncard ∈ {k}}, {x}) = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2

Tactic:
have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
        rw [mul_assoc]
        exact (memLp_one_iff_integrable.1 <| (hX.condExp one_le_two).mul hX).const_mul _

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
⊢ μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ ((partialTraj κ a (a + 1)).map fun x ↦ x ⟨a + 1, ⋯⟩) = κ a

Tactic:
have hp : (fun x : Π n : Iic (a + 1), X n ↦ x ⟨a + 1, mem_Iic.2 le_rfl⟩) ∘ IicProdIoc a (a + 1) =
      (piSingleton a).symm ∘ Prod.snd := by
    ext
    simp [_root_.IicProdIoc, piSingleton]

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hp : (fun x ↦ x ⟨a + 1, ⋯⟩) ∘ _root_.IicProdIoc a (a + 1) = ⇑(piSingleton a).symm ∘ Prod.snd
⊢ ((partialTraj κ a (a + 1)).map fun x ↦ x ⟨a + 1, ⋯⟩) = κ a
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic Kernel.id

Tactic:
unfold Kernel.id; infer_instance

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₀ : ((η ∘ₖ κ) a) s = 0
⊢ ∫⁻ (a : β) in t, (η a) s ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t

pp: case inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (a : β) in t, (η a) s ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t

Tactic:
· rw [h₀, zero_mul, setLIntegral_eq_zero_iff ht <| η.measurable_coe hs]
    rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff <| η.measurable_coe hs] at h₀
    filter_upwards [h₀] with x hx _ using hx

Goal state after:
case inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (a : β) in t, (η a) s ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t
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.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
      ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ =
    ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
rw [parallelProd_posterior_comp_copy_comp]

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

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

Tactic:
rw [parallelProd_posterior_comp_copy_comp]

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

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

Tactic:
rw [parallelProd_posterior_comp_copy_comp]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
⊢ map (⇑(piCurry X)) (infinitePi fun p ↦ μ p.fst p.snd) = infinitePi fun i ↦ infinitePi fun j ↦ μ i j

Tactic:
by
  rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_piCurry_symm]

Goal state after:
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∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ avgRisk ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π ≤ ↑C * P.bound * π Set.univ

Tactic:
refine (avgRisk_le_mul' P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π hℓC).trans ?_

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ↑C * (Kernel.const 𝓧 (Measure.dirac h𝓨.some)).bound * P.bound * π Set.univ ≤ ↑C * P.bound * π Set.univ
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(MeasurableEquiv.curry ι κ X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) = infinitePi fun p ↦ μ p.1 p.2

Tactic:
rw [← (MeasurableEquiv.piCongrLeft (fun _ ↦ X)
    (Equiv.sigmaEquivProd ι κ).symm).map_measurableEquiv_injective.eq_iff, map_map]
  · have : (MeasurableEquiv.piCongrLeft (fun _ ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘
        (MeasurableEquiv.curry ι κ X).symm = ⇑(MeasurableEquiv.piCurry (fun _ _ ↦ X)).symm := by
      ext; simp [piCongrLeft, Equiv.piCongrLeft, Sigma.uncurry]
    rw [this, infinitePi_map_piCurry_symm]
    convert! infinitePi_map_piCongrLeft (fun p ↦ μ p.1 p.2) (Equiv.sigmaEquivProd ι κ).symm |>.symm
  all_goals fun_prop

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

Goal state before:
pp: p : ↑unitInterval
⊢ IsProbabilityMeasure (geometricMeasure p)

Tactic:
geometricMeasure

Goal state after:
p : ↑unitInterval
⊢ IsProbabilityMeasure
    (if p ≠ 0 then Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n else Measure.dirac 0)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ HasPDF X ℙ μ

Tactic:
apply hasPDF_of_map_eq_withDensity (hu.aemeasurable hns hnt) (t.indicator ((μ t)⁻¹ • 1)) <|
    (measurable_one.aemeasurable.const_smul (μ t)⁻¹).indicator (measurableSet_toMeasurable μ s)

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
t : Set E := ⋯
⊢ Measure.map X ℙ = μ.withDensity (t.indicator ((μ t)⁻¹ • 1))
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
      str := Prod.instMeasurableSpace } ≅
    X

Tactic:
by
    let f₁ := fun (x : X) ↦ (PUnit.unit, x)
    have hf₁ : Measurable f₁ := by fun_prop
    have hf₂ : Measurable (Prod.snd : PUnit × X → X) := by fun_prop
    refine ⟨⟨Kernel.id.map Prod.snd, inferInstance⟩,
      ⟨Kernel.id.map f₁, inferInstance⟩, ?_, ?_⟩
    · ext : 1; dsimp
      rw [Kernel.id_map hf₁, Kernel.deterministic_comp_eq_map hf₁, Kernel.id_map hf₂,
        Kernel.deterministic_map hf₂ hf₁]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]
    · ext : 1; dsimp
      rw [Kernel.id_map hf₂, Kernel.deterministic_comp_eq_map hf₂, Kernel.id_map hf₁,
        Kernel.deterministic_map hf₁ hf₂]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]

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

Goal state before:
pp: W X Y Z : SFinKer
⊢ Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic ⇑prodAssoc ⋯ ∥ₖ Kernel.deterministic id ⋯) =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯

Tactic:
Kernel.deterministic_parallelComp_deterministic (by fun_prop) (by fun_prop)

Goal state after:
W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic ⇑prodAssoc ⋯ ∥ₖ Kernel.deterministic id ⋯) =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic ⇑prodAssoc ⋯ ∥ₖ Kernel.deterministic id ⋯) =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯

Tactic:
Kernel.deterministic_parallelComp_deterministic (by fun_prop) (by fun_prop)

Goal state after:
W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map (⇑prodAssoc) id) ⋯ =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map (⇑prodAssoc) id) ⋯ =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯

Tactic:
Kernel.deterministic_parallelComp_deterministic (by fun_prop) (by fun_prop)

Goal state after:
W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map (⇑prodAssoc) id) ⋯ =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.snd ∘ id) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.fst ∘ id) ⋯ ∥ₖ Kernel.deterministic id ⋯

Tactic:
Kernel.deterministic_parallelComp_deterministic (by fun_prop) (by fun_prop)

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.fst ∘ id) ⋯ ∥ₖ Kernel.deterministic id ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.fst ∘ id) ⋯ ∥ₖ Kernel.deterministic id ⋯

Tactic:
Kernel.deterministic_parallelComp_deterministic (by fun_prop) (by fun_prop)

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.map (Prod.fst ∘ id) id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.map (Prod.fst ∘ id) id) ⋯

Tactic:
Kernel.deterministic_parallelComp_deterministic (by fun_prop) (by fun_prop)

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.map (Prod.fst ∘ id) id) ⋯
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ (μ.tilted fun x ↦ t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ

Tactic:
tilted_apply' _ _ hs,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ ω ∈ {ω | 0 < X ω} ↔ ω ∈ ⋃ ε, {ω | ↑↑ε ≤ X ω}

Tactic:
simp only [Set.mem_ofPred_eq, Set.mem_iUnion, Subtype.exists, exists_prop]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ 0 < X ω ↔ ∃ a, 0 < a ∧ ↑a ≤ X ω
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this✝ : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
a✝ : A < x
h''x : x ≤ 0
this : x = 0
⊢ x ^ n = 0

Tactic:
simp [this, zero_pow hn]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∫ (x : ℝ) in 0..↑K, x ∂ρ ≤ ∫ (a : Ω), X a

Tactic:
← integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∫ (x : Ω), truncation X (↑K) x ≤ ∫ (a : Ω), X a