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

Goal state before:
pp: case pos.refine_2
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
⊢ 0 ≤ if ↑x < 0 then 0 else 1

Tactic:
split_ifs
      exacts [le_rfl, zero_le_one]

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

Goal state before:
pp: case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ∀ (x : { q' // ↑r < ↑q' }),
    f a ↑({ toFun := fun t ↦ ⟨↑t, ⋯⟩, invFun := fun t ↦ ⟨↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x) = f a ↑x

Tactic:
· intro t
    simp only [Equiv.coe_fn_mk, Subtype.coe_mk]

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r
r : { r' // x < ↑r' }
⊢ stieltjesFunctionAux f a ↑↑r = f a ↑r

Tactic:
exact stieltjesFunctionAux_eq hf a r

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
⊢ ρ (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) = ρ (s ×ˢ Iic r)

Tactic:
Set.prod_eq

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
⊢ ρ (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) = ρ (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
r r' : ℚ
hrr' : r ≤ r'
⊢ ∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) a, (preCDF ρ r (a, c).2).toReal ≤ (preCDF ρ r' (a, c).2).toReal

Tactic:
filter_upwards [monotone_preCDF ρ, preCDF_le_one ρ] with a h₁ h₂

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone fun r ↦ preCDF ρ r a
h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ↑I
inst✝ : IsProbabilityMeasure μ
x : ↑I
this : IsProbabilityMeasure (Measure.map Subtype.val μ)
⊢ μ.real (Subtype.val ⁻¹' Iic ↑x) = μ.real (Icc 0 x)

Tactic:
subtype_Iic_eq_Icc

Goal state after:
μ : Measure ↑I
inst✝ : IsProbabilityMeasure μ
x : ↑I
this : IsProbabilityMeasure (Measure.map Subtype.val μ)
⊢ μ.real (Icc 0 x) = μ.real (Icc 0 x)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) tᶜ ∂ν a = (κ a) (s ×ˢ tᶜ)

Tactic:
| compl t ht iht =>

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

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∫⁻ (b : β) in s, ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f i)

Tactic:
rw [lintegral_tsum, prod_iUnion, measure_iUnion]

Goal state after:
case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∑' (i : ℕ), ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, a_1)) (f i) ∂ν a = ∑' (i : ℕ), (κ a) (s ×ˢ f i)

case iUnion.hn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ Pairwise (Function.onFun Disjoint fun i ↦ s ×ˢ f i)

case iUnion.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∀ (i : ℕ), MeasurableSet (s ×ˢ f i)

case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∀ (i : ℕ), AEMeasurable (fun b ↦ ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i)) ((ν a).restrict s)
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this : ∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ = 1
⊢ ∀ᵐ (b : β) ∂κ.fst a, IsProbabilityMeasure (κCond (a, b))

Tactic:
by
    convert! this with b
    exact ⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩

Goal state after:
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
⊢ ∃ a_1,
    ∀ (b : ℕ),
      a_1 ≤ b → ∫ (x : γ) in A, κ.densityProcess ν b a x s ∂ν a = ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a

Tactic:
refine ⟨n, fun m hnm ↦ ?_⟩

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
m : ℕ
hnm : n ≤ m
⊢ ∫ (x : γ) in A, κ.densityProcess ν m a x s ∂ν a = ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν 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 α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ Measure.map (fun x ↦ (X x, Y x)) (Measure.map f ν) = Measure.map X (Measure.map f ν) ⊗ₘ condDistrib (Y ∘ f) (X ∘ f) ν

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable hX hf, compProd_map_condDistrib (by fun_prop),
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ Measure.map ((fun x ↦ (X x, Y x)) ∘ f) ν = Measure.map (fun a ↦ ((X ∘ f) a, (Y ∘ f) a)) ν
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ μ[fun a ↦ f (X a, Y a) | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a ↦ ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s < ∞
⊢ IntegrableOn (fun a ↦ ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) s μ

case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ∞ → ∫ (x : α) in s, ∫ (y : Ω), f (X x, y) ∂(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in s, f (X x, Y x) ∂μ

case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ AEStronglyMeasurable (fun a ↦ ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) μ
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ deterministic (frestrictLe₂ hba) ⋯ =
    (Kernel.id ×ₖ (deterministic (frestrictLe₂ hba) ⋯).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)

Tactic:
IicProdIoc_le hba,

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ deterministic (frestrictLe₂ hba) ⋯ =
    (Kernel.id ×ₖ (deterministic (frestrictLe₂ hba) ⋯).map (restrict₂ ⋯)).map (frestrictLe₂ hba ∘ Prod.fst)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ deterministic (frestrictLe₂ hba) ⋯ =
    (Kernel.id ×ₖ (deterministic (frestrictLe₂ hba) ⋯).map (restrict₂ ⋯)).fst.map (frestrictLe₂ hba)

pp: case inl.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst

pp: case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)

Tactic:
deterministic_map,

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ deterministic (frestrictLe₂ hba) ⋯ =
    (Kernel.id ×ₖ deterministic (restrict₂ ⋯ ∘ frestrictLe₂ hba) ⋯).fst.map (frestrictLe₂ hba)

case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (restrict₂ ⋯)

case inl.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst

case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)
Module: Mathlib.Probability.CondVar

Goal state before:
pp: case pos
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : IsFiniteMeasure μ
⊢ Var[fun x ↦ c; μ | m] = 0

pp: case neg
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : ¬IsFiniteMeasure μ
⊢ Var[fun x ↦ c; μ | m] = 0

Tactic:
· simp [condVar, hm]

Goal state after:
case neg
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : ¬IsFiniteMeasure μ
⊢ Var[fun x ↦ c; μ | m] = 0
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
⊢ map (_root_.IicProdIoc a b) ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i)) = Measure.pi fun i ↦ μ ↑i

Tactic:
IicProdIoc_le hba,

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
⊢ map (frestrictLe₂ hba ∘ Prod.fst) ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i)) = Measure.pi fun i ↦ μ ↑i
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) ↑n
⊢ (fun x ↦ f a b) =ᶠ[Filter.atTop] fun n ↦ min (f a b) ↑n

Tactic:
Filter.EventuallyEq,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) ↑n
⊢ ∀ᶠ (x : ℕ) in Filter.atTop, f a b = min (f a b) ↑x
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable fun p ↦ (κ.map fun a ↦ (a, ())).density η p.1 p.2 univ

Tactic:
exact measurable_density _ η MeasurableSet.univ

Goal state after:
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 : ℕ
hp : (fun x ↦ x ⟨a + 1, ⋯⟩) ∘ _root_.IicProdIoc a (a + 1) = ⇑(piSingleton a).symm ∘ Prod.snd
⊢ ((Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).map Prod.snd).map ⇑(piSingleton a).symm = κ a

Tactic:
← snd_eq,

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
⊢ (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).snd.map ⇑(piSingleton a).symm = κ a
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)

Tactic:
have B_eq n : B n = cylinder (t n) (T n) := by
    simp_rw [B, A_eq, cylinder, ← Set.preimage_comp, r_comp_f]; rfl

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ∫⁻ (b : γ) in s,
      ↑(κ.rnDerivAux (κ + η) a b).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b ∂(κ + η) a =
    (κ a) s

Tactic:
calc
    ∫⁻ x in s, ↑(Real.toNNReal (rnDerivAux κ (κ + η) a x)) -
      ↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) * rnDeriv κ η a x
      ∂(κ + η) a
    = ∫⁻ _ in s, 1 ∂(κ + η) a := by
        refine setLIntegral_congr_fun_ae hsm ?_
        have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
        filter_upwards [rnDerivAux_le_one h_le] with x hx hxs
        have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
        simp [h_eq_one]
  _ = (κ + η) a s := by simp
  _ = κ a s := by
        suffices η a s = 0 by simp [this]
        exact measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)

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

Goal state before:
pp: case inl
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
hbc : b ≤ c
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c

Tactic:
rw [partialTraj_comp_partialTraj hab hbc]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ (∀ (a : α), IsZeroOneMeasure (κ a)) → IsDeterministic κ

Tactic:
intro _
    refine ⟨?_⟩
    ext : 1
    rw [parallelComp_comp_copy, prod_apply]
    refine Measure.prod_eq fun s t hs ht ↦ ?_
    rw [copy_comp_apply_prod _ _ hs ht]
    exact measure_inter_eq_prod hs ht

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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measure.map (frestrictLe b) ((traj κ a) x) = (partialTraj κ a b) x

Tactic:
rw [← map_apply _ (measurable_frestrictLe b), traj_map_frestrictLe]

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)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) (⇑(piCurry X).symm ⁻¹' (↑s).pi fun x ↦ t x) =
    ∏ i ∈ s, (μ i.fst i.snd) (t i)

Tactic:
← Finset.sigma_image_fst_preimage_mk s,

Goal state after:
ι : 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)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)
      (⇑(piCurry X).symm ⁻¹' (↑((image Sigma.fst s).sigma fun a ↦ s.preimage (Sigma.mk a) ⋯)).pi fun x ↦ t x) =
    ∏ i ∈ (image Sigma.fst s).sigma fun a ↦ s.preimage (Sigma.mk a) ⋯, (μ i.fst i.snd) (t i)