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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂ν a✝ =
    ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) t₂ ∂ν a✝
a : β
hat₁ : a ∈ t₁ᶜ
⊢ ((IsCondKernelCDF.toKernel f hf) (a✝, a)) (Prod.mk a ⁻¹' t₁ ×ˢ t₂) = 0

Tactic:
rw [mem_compl_iff] at hat₁

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂ν a✝ =
    ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) t₂ ∂ν a✝
a : β
hat₁ : a ∉ t₁
⊢ ((IsCondKernelCDF.toKernel f hf) (a✝, a)) (Prod.mk a ⁻¹' t₁ ×ˢ t₂) = 0
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
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = ((κ.fst ⊗ₖ κCond).fst a) s

Tactic:
fst_compProd_apply _ _ _ hs

Goal state after:
α : 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
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a =
    ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.right
α : 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
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
h_2_le : (s.indicator fun b ↦ (κCond (a, b)) univ) ≤ s.indicator fun x ↦ r
⊢ (κ.fst a) {x | (κCond (a, x)) univ ≤ r} = 0

Tactic:
have : κ.fst a s ≤ ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) :=
      (h_eq s hs).symm.trans_le (lintegral_mono h_2_le)

Goal state after:
case pos.right
α : 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
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
h_2_le : (s.indicator fun b ↦ (κCond (a, b)) univ) ≤ s.indicator fun x ↦ r
this : (κ.fst a) s ≤ ∫⁻ (b : β), s.indicator (fun x ↦ r) b ∂κ.fst a
⊢ (κ.fst a) {x | (κCond (a, x)) univ ≤ r} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : (ν a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤
    ((κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤
    ((κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal

Tactic:
· rw [h0, ENNReal.toReal_div, ENNReal.toReal_div]
    simp

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤
    ((κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hb
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 : ¬(ν a) (countablePartitionSet n x) = 0
h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
⊢ (κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ≠ ∞

Tactic:
simp only [ne_eq, ENNReal.div_eq_top, h0, and_false, false_or, not_and, not_not]
    exact fun h_top ↦ eq_top_mono h_le h_top

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

Goal state before:
pp: case hb
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν ν' : Kernel α γ
hνν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ≠ ∞

Tactic:
simp only [ne_eq, ENNReal.div_eq_top, h0, and_false, false_or, not_and, not_not]
    exact fun h_top ↦ eq_top_mono h_le h_top

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

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

Tactic:
rw [← setLIntegral_condKernel hf MeasurableSet.univ ht]

Goal state after:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
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 Ω
κ : Kernel α (γ × Ω)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelBorel = κ

Tactic:
by
    rw [condKernelBorel, compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelReal _)]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 < ∞ →
        ∫ (x : α) in s_1, ((condDistrib Y X μ) (X x)).real s ∂μ = ∫ (x : α) in s_1, (Y ⁻¹' s).indicator (fun ω ↦ 1) x ∂μ

Tactic:
intro t ht _

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in t, ((condDistrib Y X μ) (X x)).real s ∂μ = ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun ω ↦ 1) x ∂μ
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) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (μ[X | m] ^ 2) μ
ω : Ω
hω₀ : μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 - 2 * X * μ[X | m] | m] + μ[μ[X | m] ^ 2 | m]) ω
hω₁ : μ[X ^ 2 - 2 * X * μ[X | m] | m] ω = (μ[X ^ 2 | m] - μ[2 * X * μ[X | m] | m]) ω
hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω
⊢ μ[OfNat.ofNat 2 * X | m] ω = (OfNat.ofNat 2 * μ[X | m]) ω →
    μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2) ω

Tactic:
hω₃

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]) μ
aux₂ : Integrable (μ[X | m] ^ 2) μ
ω : Ω
hω₀ : μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 - 2 * X * μ[X | m] | m] + μ[μ[X | m] ^ 2 | m]) ω
hω₁ : μ[X ^ 2 - 2 * X * μ[X | m] | m] ω = (μ[X ^ 2 | m] - μ[2 * X * μ[X | m] | m]) ω
hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω
hω₃ : μ[OfNat.ofNat 2 * X | m] ω = (OfNat.ofNat 2 * μ[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.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)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (map (I.preimage ⇑e ⋯).restrict (infinitePiNat fun n ↦ μ (e n)))
      (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S) =
    (piContent μ) (I.restrict ⁻¹' S)

pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable (I.preimage ⇑e ⋯).restrict

pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ MeasurableSet (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S)

pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ MeasurableSpace ((a : ↥(I.preimage ⇑e ⋯)) → X ↑((e.restrictPreimageFinset I) a))

pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)

Tactic:
infinitePiNat_map_restrict (fun n ↦ μ (e n)),

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ (Measure.pi fun i ↦ μ (e ↑i)) (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S) =
    (piContent μ) (I.restrict ⁻¹' S)

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable (I.preimage ⇑e ⋯).restrict

case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ MeasurableSet (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S)

ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
x₀ : (i : ↥(Iic a)) → X ↑i
hbc : b ≤ c
⊢ Measure.map (frestrictLe₂ hbc) ((partialTraj κ a c) x₀) = (partialTraj κ a b) x₀

Tactic:
by
  rw [← map_apply _ (by fun_prop), partialTraj_map_frestrictLe₂]

Goal state after:
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 : α
h_ac : κ a ≪ η a
c : γ
hc : κ.rnDeriv η a c = (∂κ a/∂η a) c
⊢ (∂κ a/∂η a) c = 1 ↔ (∂κ a/∂η a) c = 1 c

Tactic:
Pi.one_apply

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_ac : κ a ≪ η a
c : γ
hc : κ.rnDeriv η a c = (∂κ a/∂η a) c
⊢ (∂κ a/∂η a) c = 1 ↔ (∂κ a/∂η a) c = 1
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ ⇑Kernel.id ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ

Tactic:
Measure.id_comp

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : StandardBorelSpace Ω
inst✝ : Nonempty Ω
⊢ μ ⊗ₘ κ = μ ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
this : ⇑Kernel.id =ᵐ[⇑Kernel.id ∘ₘ μ] ⇑(Kernel.id†μ)
⊢ ⇑(Kernel.id†μ) =ᵐ[μ] ⇑Kernel.id

Tactic:
Measure.id_comp

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
this : ⇑Kernel.id =ᵐ[μ] ⇑(Kernel.id†μ)
⊢ ⇑(Kernel.id†μ) =ᵐ[μ] ⇑Kernel.id
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ partialTraj κ b a = deterministic (frestrictLe₂ hab) ⋯

Tactic:
partialTraj_le

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ deterministic (frestrictLe₂ ?m.67) ⋯ = deterministic (frestrictLe₂ hab) ⋯

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
⊢ a ≤ b
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
⊢ μ ⊗ₘ κ = ⇑Kernel.id ∘ₘ μ ⊗ₘ κ

Tactic:
Measure.id_comp

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
⊢ μ ⊗ₘ κ = μ ⊗ₘ κ
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n k : ℕ
p : ↑I
⊢ Bin(R, n, p).real {↑k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

Tactic:
rw [map_measureReal_apply (by fun_prop) (by measurability)]
  convert binomial_real_singleton n k p
  ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝² : MeasurableSpace R
inst✝¹ : AddMonoidWithOne R
inst✝ : MeasurableSingletonClass R
n : ℕ
p : ↑I
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.Iic n
⊢ map Nat.cast (ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • dirac x✝¹) =
    ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • dirac ↑x✝¹

Tactic:
rw [Measure.map_smul, map_dirac]

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

Goal state before:
pp: p : ↑unitInterval
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < (geometricMeasure p).real {n}

Tactic:
rw [geometricMeasure_real_singleton h1]

Goal state after:
p : ↑unitInterval
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < (1 - ↑p) ^ n * ↑p
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))

Tactic:
have _ : 0 < x := by linarith

Goal state after:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
x✝ : 0 < x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 1 - rexp (-(r * x))

Tactic:
simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff]

Goal state after:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ r * x
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
h : μ {ω | X ω = 1} = ⊤
⊢ ∫ (y : ℝ), id y ∂(μ (X ⁻¹' {0}) • Measure.dirac 0 + μ (X ⁻¹' {1}) • Measure.dirac 1) = μ.real {ω | X ω = 1}

Tactic:
simp [h, Measure.real, Set.preimage, integral_undef, Integrable, HasFiniteIntegral]

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ 0 ≤ poissonPMFReal r n

Tactic:
unfold poissonPMFReal
  positivity

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

Goal state before:
pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ 1 - μ[X | m] =ᵐ[μ] μ[1 - X | m]

Tactic:
calc
        1 - μ[X | m]
        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
        _ =ᵐ[μ] μ[1 - X | m] := by
          refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
          filter_upwards [hX]
          rintro ω (hω | hω) <;> simp [hω]

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

Goal state before:
pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ iIndepFun (fun j ω ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i))

Tactic:
rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)]

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ map (fun ω i_1 ↦ X i i_1 (ω i i_1)) (infinitePi fun i ↦ infinitePi (μ i)) =
    infinitePi fun i_1 ↦ map (fun ω ↦ X i i_1 (ω i i_1)) (infinitePi fun i ↦ infinitePi (μ i))
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            ((condExpKernel μ m') a) (t1 ∩ t2) = ((condExpKernel μ m') a) t1 * ((condExpKernel μ m') a) t2) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
have hs2_eq : ∀ s ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s | m'⟧ :=
    fun s hs ↦ condExpKernel_ae_eq_condExp hm' (hs2 s hs)

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            ((condExpKernel μ m') a) (t1 ∩ t2) = ((condExpKernel μ m') a) t1 * ((condExpKernel μ m') a) t2) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), c * (A.indicator 1 x * f x) ∂π x₀ = c * (A.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀)

Tactic:
rw [lintegral_const_mul, hπ.lintegral_indicator_mul h𝓑𝓧 hf hA]

Goal state after:
case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ A.indicator 1 x * f x