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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
x : β × Ω
⊢ x ∈ Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ ↔ x ∈ ∅

Tactic:
simp

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

Goal state before:
pp: case h_empty
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, (κ x) ∅ = (ρ.condKernel x) ∅

Tactic:
simp

Goal state after:
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 α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : (ν a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ ((κ a) (countablePartitionSet n x ×ˢ seq m)).toReal / ENNReal.toReal 0) atTop
    (𝓝 (((κ a) (countablePartitionSet n x ×ˢ ∅)).toReal / ENNReal.toReal 0))

Tactic:
simp

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ ∅) ≠ 0 → (ν a) (countablePartitionSet n x) ≠ 0) ∧
    ((κ a) (countablePartitionSet n x ×ˢ ∅) = ∞ → (ν a) (countablePartitionSet n x) = ∞)

Tactic:
simp

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

Goal state before:
pp: case refine_2.refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ 0 ≤ ENNReal.ofReal ε

Tactic:
simp

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 ≤ ν
a : α
inst✝ : IsFiniteKernel ν
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : γ) ∂ν a, Tendsto (fun n ↦ κ.densityProcess ν n a x s) atTop (𝓝 (κ.density ν a x s))

Tactic:
filter_upwards [tendsto_densityProcess_limitProcess hκν a hs, density_ae_eq_limitProcess hκν a hs]
    with t h1 h2 using h2 ▸ h1

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
s : Set β
⊢ (ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
this : ⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) =ᵐ[Measure.map (AEMeasurable.mk X hX) μ] ⇑κ
⊢ ⇑(condDistrib Y X μ) =ᵐ[Measure.map (AEMeasurable.mk X hX) μ] ⇑κ

Tactic:
condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
this : ⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) =ᵐ[Measure.map (AEMeasurable.mk X hX) μ] ⇑κ
⊢ ⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) =ᵐ[Measure.map (AEMeasurable.mk X hX) μ] ⇑κ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
⊢ ∫ (x : γ) in ∅, κ.density ν a x s ∂ν a = (κ a).real (∅ ×ˢ s)

Tactic:
simp

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 ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
⊢ (univ \ A) ×ˢ s = univ ×ˢ (s \ s) ∪ (univ \ A) ×ˢ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ✝ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ✝
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
h1 : const Unit ρ.fst = (const Unit ρ).fst
h2 : prodMkLeft Unit ρ.condKernel = (const Unit ρ).condKernelUnitBorel
⊢ (const Unit ρ) () = ρ

Tactic:
simp

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 ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
a✝ : γ × β
⊢ a✝ ∈ A ×ˢ s → a✝ ∈ univ ×ˢ s

Tactic:
simp

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 ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
x : γ × β
⊢ x ∈ A ×ˢ s → x ∈ univ ×ˢ s

Tactic:
simp

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 : ι
i : ↥(Ioc a c)
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i

Tactic:
by_cases h : i ≤ b

Goal state after:
case pos
ι : 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)
h : ↑i ≤ b
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i

case neg
ι : 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)
h : ¬↑i ≤ b
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i
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κν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ (κ a) (univ ×ˢ s) ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ A ⊆ univ

Tactic:
simp

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✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a : ι
x : (n : ι) → X n
⊢ (fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩) ((fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i)) x) = x

Tactic:
simp

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
x : X (a + 1)
⊢ (fun x ↦ x ⟨a + 1, ⋯⟩) ((fun x i ↦ ⋯ ▸ x) x) = x

Tactic:
simp

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
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
x : ((i : ↥(Ioc a b)) → X ↑i) × ((i : ↥(Ioc b c)) → X ↑i)
⊢ x ∈ IocProdIoc a b c ⁻¹' Set.univ.pi s ↔ x ∈ Set.univ.pi (restrict₂ ⋯ s) ×ˢ Set.univ.pi (restrict₂ ⋯ s)

Tactic:
simp

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : DecidableLE ι
X : ι → Type u_2
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
x : ((i : ↥(Ioc a b)) → X ↑i) × ((i : ↥(Ioc b c)) → X ↑i)
⊢ (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ c), IocProdIoc a b c x ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ↔
    (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ b), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ∧
      ∀ (a_1 : ι) (hp : b < a_1) (hq : a_1 ≤ c), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in t, ((condDistrib Y X μ) (X a)) s ∂μ = μ (t ∩ Y ⁻¹' s)

Tactic:
by
  obtain ⟨t', ht', rfl⟩ := ht
  rw [setLIntegral_preimage_condDistrib hX hY hs ht']

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

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

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : (κ.fst a) (countablePartitionSet n x) = 0
h' : ¬(κ a) (countablePartitionSet n x ×ˢ univ) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / 0).toReal = 0

Tactic:
simp

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 α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x✝ : γ
h : ¬(κ.fst a) (countablePartitionSet n x✝) = 0
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ univ ↔ x ∈ {p | p.1 ∈ countablePartitionSet n x✝}

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ ENNReal.toReal 1 = 1

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case neg
β : 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 μ
⊢ 0 (Prod.snd ⁻¹' s) = 0

Tactic:
simp

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 α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ ∑' (p : ↑(countablePartition γ n)), (κ.fst a) (⋃ (_ : (κ.fst a) ↑p = 0), ↑p) = 0

Tactic:
simp

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

Goal state before:
pp: case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) 0

Tactic:
simp

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

Goal state before:
pp: case inr.base
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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Kernel.id x = Measure.map (_root_.IicProdIoc a a) ((Kernel.id x).prod ((deterministic (restrict₂ ⋯) ?inr.base✝) x))

pp: case inr.base.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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a a)

pp: case inr.base
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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)

Tactic:
IicProdIoc_self,

Goal state after:
case inr.base
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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Kernel.id x = Measure.map Prod.fst ((Kernel.id x).prod ((deterministic (restrict₂ ⋯) ?inr.base✝) x))

case inr.base.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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a a)

case inr.base
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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
⊢ (∀ ⦃n : ℕ⦄, 0 ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)) ↔ ∀ (n : ℕ), Measure.map (frestrictLe n) ν = μ (Iic n)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ (↑this.toFinset).PairwiseDisjoint singleton

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ ∀ b ∈ this.toFinset, MeasurableSet {b}

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
⊢ (map Set.ncard setBer(u, p)) {k} ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case hz
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
⊢ Nonempty (X 0)

Tactic:
exact ⟨y ⟨0, mem_Iic.2 zero_le⟩⟩

Goal state after:
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: V : Type u_1
p : ↑I
inst✝ : Finite V
G : SimpleGraph V
val✝ : Fintype V
⊢ G.edgeSet ⊆ Sym2.diagSetᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (1 a✝¹)) s✝ = (κ a✝¹) s✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (0 a✝¹)) s✝ = (0 a✝¹) s✝

Tactic:
simp

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

Goal state before:
pp: case zero
α : 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 : β
⊢ ∑ i ∈ Finset.range 0, fs i a b = min (f a b) ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case neg
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
hs : ¬s.Nonempty
⊢ (((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯)) x) ∅ =
    ((const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x) ∅

Tactic:
simp

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

Goal state before:
pp: case neg.e_6
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
x : γ
⊢ x ∈ (fun a ↦ (a, ())) ⁻¹' s ×ˢ univ ↔ x ∈ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η
a : α
s : Set γ
a✝ : MeasurableSet s
⊢ ((κ + η) a) s = (κ a) s + (η a) s

Tactic:
simp

Goal state after: