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

Goal state before:
pp: case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ x_1, ↑(s x_1) < x

Tactic:
tendsto_atTop_atBot

Goal state after:
case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ x_1, ↑(s x_1) < x
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop =
    limsup (fun x ↦ ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a) atTop

Tactic:
limsup_congr

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ limsup ?m.170 atTop = limsup (fun x ↦ ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a) atTop

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ ∀ᶠ (a_1 : ℕ) in atTop, ∫ (x : γ) in A, κ.densityProcess ν a_1 a x s ∂ν a = ?m.170 a_1

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ ℕ → ℝ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
h : Tendsto (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop (𝓝 (∫ (x : γ) in A, κ.density ν a x s ∂ν a))
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop

Tactic:
rw [h.limsup_eq]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (X i)
a b c : ι
⊢ Measurable (IocProdIoc a b c)

Tactic:
refine measurable_pi_lambda _ (fun i ↦ ?_)

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
m n : ι
⊢ Measurable (IicProdIoc m n)

Tactic:
refine measurable_pi_lambda _ (fun i ↦ ?_)

Goal state after:
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
m n : ι
i : ↥(Iic n)
⊢ Measurable fun c ↦ IicProdIoc m n c i
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a : ι
⊢ Measurable
    ⇑{ toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }

Tactic:
refine measurable_pi_lambda _ (fun i ↦ ?_)

Goal state after:
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }
      c i
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
k : ℕ
hak : a ≤ k
hk :
  Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1))
⊢ Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    (Kernel.id ×ₖ (κ (k + 1)).map ⇑(piSingleton (k + 1)) ∘ₖ partialTraj κ a (k + 1)).map
      (_root_.IicProdIoc (k + 1) (k + 1 + 1))

Tactic:
| succ k hak hk =>

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

Goal state before:
pp: case pos.hs
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
m n : ℕ
hmn : m ≤ n
y : (n : ℕ) → X n
⊢ χ n y ≤ χ m y

Tactic:
apply Set.indicator_le fun a ha ↦ ?_

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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a✝ : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a✝ n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a✝ n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a✝ n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a✝ n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a✝ n) (χ n) (updateFinset y (Iic p) x₀)
m n : ℕ
hmn : m ≤ n
y a : (n : ℕ) → X n
ha : a ∈ A n
⊢ 1 a ≤ χ m a
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x

Tactic:
by
  rw [mutuallySingularSetSlice, mem_ofPred]

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

Goal state before:
pp: case inl.inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab hbc : a ≤ a
⊢ lmarginalPartialTraj κ a a (lmarginalPartialTraj κ a a f) x₀ = lmarginalPartialTraj κ a a f x₀

Tactic:
lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)

Goal state after:
case inl.inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab hbc : a ≤ a
⊢ lmarginalPartialTraj κ a a f x₀ = lmarginalPartialTraj κ a a f x₀
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl.inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a ≤ a
hbc✝ : a ≤ c
hbc : a < c
⊢ lmarginalPartialTraj κ a a (lmarginalPartialTraj κ a c f) x₀ = lmarginalPartialTraj κ a c f x₀

Tactic:
lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)

Goal state after:
case inl.inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a ≤ a
hbc✝ : a ≤ c
hbc : a < c
⊢ lmarginalPartialTraj κ a c f x₀ = lmarginalPartialTraj κ a c f x₀
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Set ι
s : Finset ↑I
t : (i : ↑I) → Set (X ↑i)
ht : ∀ (i : ↑I), MeasurableSet (t i)
⊢ (infinitePi μ) (I.domRestrict ⁻¹' (↑s).pi t) = ∏ i ∈ s, (μ ↑i) (t i)

pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Set ι
s : Finset ↑I
t : (i : ↑I) → Set (X ↑i)
ht : ∀ (i : ↑I), MeasurableSet (t i)
⊢ MeasurableSet ((↑s).pi t)

Tactic:
domRestrict_preimage,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Set ι
s : Finset ↑I
t : (i : ↑I) → Set (X ↑i)
ht : ∀ (i : ↑I), MeasurableSet (t i)
⊢ (infinitePi μ) ((↑(image Subtype.val s)).pi fun i ↦ if h : i ∈ I then t ⟨i, h⟩ else Set.univ) = ∏ i ∈ s, (μ ↑i) (t i)

ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Set ι
s : Finset ↑I
t : (i : ↑I) → Set (X ↑i)
ht : ∀ (i : ↑I), MeasurableSet (t i)
⊢ MeasurableSet ((↑s).pi t)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case compl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
mt : MeasurableSet t
ht : Measurable fun x₀ ↦ (trajFun κ a x₀) t
⊢ Measurable fun x₀ ↦ (trajFun κ a x₀) tᶜ

Tactic:
have := isProbabilityMeasure_trajFun κ a

Goal state after:
case compl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
mt : MeasurableSet t
ht : Measurable fun x₀ ↦ (trajFun κ a x₀) t
this : ∀ (x₀ : (i : ↥(Iic a)) → X ↑i), IsProbabilityMeasure (trajFun κ a x₀)
⊢ Measurable fun x₀ ↦ (trajFun κ a x₀) tᶜ
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : 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
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ ∫⁻ (x : β), (η x) sᶜ ∂κ a = ((η ∘ₖ κ) a) sᶜ

Tactic:
by
        rw [η.comp_apply' _ _ hs.compl]

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∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ ∫⁻ (x : 𝓨), ∫⁻ (θ : Θ), ℓ θ x * (P θ) Set.univ ∂π ∂μ = ∫⁻ (θ : Θ), (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂μ ∂π

Tactic:
rw [lintegral_lintegral_swap]

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ ∫⁻ (y : Θ), ∫⁻ (x : 𝓨), ℓ y x * (P y) Set.univ ∂μ ∂π = ∫⁻ (θ : Θ), (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂μ ∂π

case hf
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ AEMeasurable (uncurry fun x θ ↦ ℓ θ x * (P θ) Set.univ) (μ.prod π)
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
a : α
h : MeasurableSet {a}
⊢ p.toMeasure {a} = p a

Tactic:
by
  simp [p.toMeasure_apply_eq_toOuterMeasure_apply h, toOuterMeasure_apply_singleton]

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

Goal state before:
pp: case refine_1
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₀))
t : Set ((i : ↥(Iic b)) → X ↑i)
mt : MeasurableSet t
⊢ ∫ (x : (i : ℕ) → X i) in frestrictLe b ⁻¹' t,
      ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) x ∂(traj κ a) x₀ =
    ∫ (x : (i : ℕ) → X i) in frestrictLe b ⁻¹' t, f x ∂(traj κ a) x₀

Tactic:
Function.comp_apply

Goal state after:
case refine_1
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₀))
t : Set ((i : ↥(Iic b)) → X ↑i)
mt : MeasurableSet t
⊢ ∫ (x : (i : ℕ) → X i) in frestrictLe b ⁻¹' t,
      ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) (frestrictLe b x) ∂(traj κ a) x₀ =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' t, f y ∂(traj κ a) x₀
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
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
by_cases hnt : μ s = ∞

Goal state after:
case pos
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
⊢ ∫ (x : Ω), X x ∂ℙ = (volume s)⁻¹.toReal * ∫ (x : ℝ) in s, x

Tactic:
by
  rw [← smul_eq_mul, ← integral_smul_measure]
  dsimp only [IsUniform, ProbabilityTheory.cond] at huX
  rw [← huX]
  by_cases hX : AEMeasurable X ℙ
  · exact (integral_map hX aestronglyMeasurable_id).symm
  · rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable]
    rwa [aestronglyMeasurable_iff_aemeasurable]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h1 : iIndepFun X P
h2 : AEMeasurable (fun ω i ↦ X i ω) P
this : IsProbabilityMeasure P
⊢ (infinitePi fun i ↦ map (X i) P) = infinitePi μ

Tactic:
fun i ↦ (hX i).map_eq

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (fun ω i ↦ X i ω) P
h : HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P
⊢ infinitePi μ = infinitePi fun i ↦ map (X i) P

Tactic:
fun i ↦ (hX i).map_eq

Goal state after:
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✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
this : {x | τ x = ↑i} = ∅
⊢ μ[f n | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] f i

Tactic:
by simp [this]; norm_cast

Goal state after:
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
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
x : Ω
hx : τ x ≤ σ x → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
hx_mem : x ∈ {ω | σ ω ≤ τ ω}ᶜ
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
simp only [Set.mem_compl_iff, Set.mem_ofPred_eq, not_le] at hx_mem

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
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
x : Ω
hx : τ x ≤ σ x → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
hx_mem : τ x < σ x
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] Z

Tactic:
by
  suffices (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] (fun ω (_ : Unit) ↦ Z ω) from
    this.comp (measurable_id) (measurable_pi_apply ())
  refine indicator_indepFun_pi_of_prod_bcf mA (fun _ ↦ mZ) fun f ↦ ?_
  convert! h (f ()) <;> simp

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in 0..A, y ∂Measure.map f μ

Tactic:
simpa using moment_truncation_eq_intervalIntegral_of_nonneg hf one_ne_zero h'f

Goal state after: