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

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst✝ : IsSFiniteKernel η
⊢ deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) = Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ))

Tactic:
ext x s ms

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst✝ : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
⊢ ((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ)) x) s = ((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ))) x) s
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (a : Ω), (μ[X | m] ^ 2) a ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), μ[X | m] x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (μ[X | m] ^ 2) μ

Tactic:
integral_condExp hm

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (a : Ω), (μ[X | m] ^ 2) a ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (μ[X | m] ^ 2) μ
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ ∫ (b : β), f b ∂(κ.withDensity fun a b ↦ ↑(g a b)) a = ∫ (b : β), g a b • f b ∂κ a

Tactic:
rw [Kernel.withDensity_apply, integral_withDensity_eq_integral_smul]
  · fun_prop
  · fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a a.succ).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

Tactic:
ext1 x₀

Goal state after:
case inl.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ ((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a a.succ).map (restrict₂ ⋯)) x₀ =
    (const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x₀
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a (n + 1)).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

Tactic:
ext1 x₀

Goal state after:
case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ ((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a (n + 1)).map (restrict₂ ⋯)) x₀ =
    (const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x₀
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b ↦ f n a b) b ∂κ a
⊢ ∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s

Tactic:
congr with n

Goal state after:
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b ↦ f n a b) b ∂κ a
n : ι
⊢ ∫⁻ (a_1 : β) in s, f n a a_1 ∂κ a = ((κ.withDensity (f n)) a) s
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

Tactic:
ext x s ms

Goal state after:
case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X ↑i
s : Set ((i : ↥(Ioc a b)) → X ↑i)
ms : MeasurableSet s
⊢ (((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯)) x) s =
    ((const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x) s
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c

Tactic:
by
  obtain hbc | hcb := le_total b c
  · rw [partialTraj_comp_partialTraj hab hbc]
  · rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]

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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ℕ → Set ((i : ℕ) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ i, f i ∈ measurableCylinders X
hf' : Pairwise (Disjoint on f)
⊢ ∀ ⦃s : ℕ → Set ((i : ℕ) → X i)⦄,
    (∀ (n : ℕ), s n ∈ measurableCylinders X) →
      Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ (trajContent κ x₀) (s n)) atTop (𝓝 0)

Tactic:
exact fun s hs anti_s inter_s ↦ trajContent_tendsto_zero hs anti_s inter_s x₀

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: 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)))

pp: 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)))

Tactic:
· conv in ∏ _ ∈ _, _ =>
      rw [← infinitePi_pi _ (by measurability), ← infinitePi_map_restrict', map_apply
        (by fun_prop) (by apply MeasurableSet.pi (countable_toSet _) (by measurability)),
        domRestrict_preimage]
      simp only [coe_image, dite_eq_ite]
    have : s.pi t
      = ⋂ s' : Finset s,
        (Subtype.val '' (s' : Set s)).pi (fun i ↦ if i ∈ s then t i else Set.univ) := by
      rw [← Set.pi_iUnion_eq_iInter_pi, Set.iUnion_finset_eq_set]
      grind
    rw [this]
    apply tendsto_measure_iInter_atTop
    · refine fun s' ↦ MeasurableSet.nullMeasurableSet (MeasurableSet.pi ?_ (by measurability))
      exact (Finset.countable_toSet _).image _
    · intro _ _ h
      simpa using Set.pi_mono' (by simp) (Set.image_mono h)
    · exact ⟨{Nonempty.some s_ne}, by simp⟩

Goal state after:
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.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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂(traj κ a) x₀ = ∫⁻ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) x₀

Tactic:
← traj_map_updateFinset,

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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀) =
    ∫⁻ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) x₀
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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ ∫ (x : (n : ℕ) → X n), f x ∂(traj κ a) x₀ = ∫ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) x₀

Tactic:
← traj_map_updateFinset,

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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ ∫ (x : (n : ℕ) → X n), f x ∂Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀) =
    ∫ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) x₀
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
⊢ ((traj κ b) x) (Prod.mk x ⁻¹' s) = ((traj κ b) x) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

Tactic:
← traj_map_updateFinset,

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
⊢ (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)
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
⊢ cauchyPDFReal x₀ 0 = 0

Tactic:
by
  ext
  simp [cauchyPDFReal]

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
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
⊢ ((traj κ a) x₀)[f | ↑piLE b] =ᵐ[(traj κ a) x₀] fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) (frestrictLe b x)

Tactic:
have i_f' : Integrable (fun x ↦ ∫ y, f y ∂(traj κ b) x)
      (((traj κ a) x₀).map (frestrictLe b)) := by
    rw [← map_apply _ (measurable_frestrictLe _), traj_map_frestrictLe _ _]
    rw [← traj_comp_partialTraj hab] at i_f
    exact i_f.integral_comp

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)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ ((traj κ a) x₀)[f | ↑piLE b] =ᵐ[(traj κ a) x₀] fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) (frestrictLe b x)
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, p x = 0

Tactic:
exact fun a ha => (p.apply_eq_zero_iff a).2 <| Set.notMem_subset h ha

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ (p.toMeasure.restrict p.support) s = p.toMeasure s

Tactic:
Measure.restrict_apply hs,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ p.toMeasure (s ∩ p.support) = p.toMeasure s
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
⊢ ∑' (i : ℕ), (ENNReal.ofReal ((1 - ↑p) ^ i * ↑p)).toReal • f i = ∑' (n : ℕ), ((1 - ↑p) ^ n * ↑p) • f n

Tactic:
congr with n

Goal state after:
case e_f
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n = ((1 - ↑p) ^ n * ↑p) • f n
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ Po(r).real {n} = rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
rw [measureReal_def, poissonMeasure_singleton, ENNReal.toReal_ofReal (by positivity)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
⊢ ∑' (a : α), p a * q x = q x

Tactic:
ENNReal.tsum_mul_right,

Goal state after:
α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
⊢ (∑' (i : α), p i) * q x = q x
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ ∑' (i : ℕ), (ENNReal.ofReal (rexp (-↑r) * ↑r ^ i / ↑i !)).toReal • f i =
    ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f n

Tactic:
congr with n

Goal state after:
case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n = (rexp (-↑r) * ↑r ^ n / ↑n !) • f n
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ (map f p).toMeasure s = p.toMeasure (f ⁻¹' s)

Tactic:
rw [toMeasure_apply_eq_toOuterMeasure_apply _ hs,
    toMeasure_apply_eq_toOuterMeasure_apply _ (measurableSet_preimage hf hs)]
  exact toOuterMeasure_map_apply f p s

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a

Tactic:
simp only [ENNReal.tsum_eq_zero]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) a_1) = 0 then 0 else (g a_1 ⋯) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ Integrable (fun ω ↦ ((condExpKernel μ m) ω).real s) μ

Tactic:
by
  nontriviality Ω
  rw [condExpKernel_eq]
  exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω ↦ ((condExpKernel μ m) ω).real s) =ᵐ[μ.trim hm] μ[s.indicator fun ω ↦ 1 | m]

Tactic:
simp_rw [measureReal_def]
  rw [(measurable_condExpKernel hs).ennreal_toReal.stronglyMeasurable.ae_eq_trim_iff hm
    stronglyMeasurable_condExp]
  exact condExpKernel_ae_eq_condExp hm hs

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

Goal state before:
pp: X : SFinKer
⊢ StochHom (𝟙 X)

Tactic:
dsimp [StochHom]

Goal state after:
X : SFinKer
⊢ IsMarkovKernel Kernel.id
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X✝ Y✝ Z✝ : SFinKer
κ : X✝ ⟶ Y✝
η : Y✝ ⟶ Z✝
hκ : StochHom κ
hη : StochHom η
⊢ StochHom (κ ≫ η)

Tactic:
dsimp [StochHom]

Goal state after:
X✝ Y✝ Z✝ : SFinKer
κ : X✝ ⟶ Y✝
η : Y✝ ⟶ Z✝
hκ : StochHom κ
hη : StochHom η
⊢ IsMarkovKernel (η.hom ∘ₖ κ.hom)
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y Z : SFinKer
κ : Y ⟶ Z
hκ : StochHom κ
⊢ StochHom (X ◁ κ)

Tactic:
dsimp [StochHom]

Goal state after:
X Y Z : SFinKer
κ : Y ⟶ Z
hκ : StochHom κ
⊢ IsMarkovKernel (Kernel.id ∥ₖ κ.hom)
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X₁✝ X₂✝ : SFinKer
κ : X₁✝ ⟶ X₂✝
hκ : StochHom κ
Y : SFinKer
⊢ StochHom (κ ▷ Y)

Tactic:
dsimp [StochHom]

Goal state after:
X₁✝ X₂✝ : SFinKer
κ : X₁✝ ⟶ X₂✝
hκ : StochHom κ
Y : SFinKer
⊢ IsMarkovKernel (κ.hom ∥ₖ Kernel.id)
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X : SFinKer
⊢ StochHom ε

Tactic:
dsimp [StochHom]

Goal state after:
X : SFinKer
⊢ IsMarkovKernel (Kernel.discard X.carrier)
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X : SFinKer
⊢ StochHom Δ

Tactic:
dsimp [StochHom]

Goal state after:
X : SFinKer
⊢ IsMarkovKernel (copy X.carrier)
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']

Tactic:
have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
        intro i hi
        rw [(h_sets i hi).choose_spec.2.symm]
        simp only [g, dif_pos hi]

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
⊢ StronglyMeasurable fun ω ↦ edist (X s ω) (X t ω)

Tactic:
borelize (E × E)

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ StronglyMeasurable fun ω ↦ edist (X s ω) (X t ω)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (-X) ω)) (⇑κ ∘ₘ ν)

Tactic:
by simpa using h.integrable_exp_mul (-t)

Goal state after:
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 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, X =ᵐ[κ ω'] 0

Tactic:
filter_upwards [(h.neg).measure_pos_eq_zero_of_hasSubGaussianMGF_zero,
    h.measure_pos_eq_zero_of_hasSubGaussianMGF_zero]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ (a : Ω'), (κ a) {ω | 0 < (-X) ω} = 0 → (κ a) {ω | 0 < X ω} = 0 → X =ᵐ[κ a] 0