mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ IocProdIoc a b c ⁻¹' Set.univ.pi s = Set.univ.pi (restrict₂ ⋯ s) ×ˢ Set.univ.pi (restrict₂ ⋯ s)

Tactic:
ext x

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

Tactic:
ext x

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
⊢ x ∈ IicProdIoc a b ⁻¹' Set.univ.pi s ↔ x ∈ Set.univ.pi (frestrictLe₂ hab s) ×ˢ Set.univ.pi (restrict₂ ⋯ s)
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
⊢ countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}

Tactic:
ext x

Goal state after:
α : 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✝}
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}
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}).toReal = 1

Tactic:
rw [this, ENNReal.div_self]

Goal state after:
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

case neg.h0
α : 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}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0

case neg.hI
α : 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}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n 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 α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
t : γ
ht : (κ.fst a) (countablePartitionSet n t) = 0
⊢ ∃ i ∈ countablePartition γ n, (κ.fst a) i = 0 ∧ t ∈ i

Tactic:
exact ⟨countablePartitionSet n t, countablePartitionSet_mem _ _, ht,
      mem_countablePartitionSet _ _⟩

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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
this : ∀ (m : ℕ), (κ a) (countablePartitionSet n x ×ˢ seq m) = 0
⊢ countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x✝ : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x✝} = 0
this : ∀ (m : ℕ), (κ a) (countablePartitionSet n x✝ ×ˢ seq m) = 0
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ univ ↔ x ∈ {p | p.1 ∈ countablePartitionSet n 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 α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
have h := fun n ↦ densityProcess_fst_univ_ae κ n a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ (n : ℕ), ∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ (n : ℕ), Integrable (fun x ↦ κ.density κ.fst a x (seq n)) (κ.fst a)

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 (∫ (a : γ), 1 ∂κ.fst a))

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂κ.fst a, Monotone fun i ↦ κ.density κ.fst a a_1 (seq i)

pp: case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.density κ.fst a a_1 (seq i) ≤ 1

Tactic:
· exact fun m ↦ integrable_density le_rfl _ (hseq_meas m)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 (∫ (a : γ), 1 ∂κ.fst a))

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂κ.fst a, Monotone fun i ↦ κ.density κ.fst a a_1 (seq i)

case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.density κ.fst a a_1 (seq i) ≤ 1
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_cyl : ∀ (n : ℕ), ∃ a S, MeasurableSet S ∧ A n = cylinder (Iic a) S
⊢ Tendsto (fun n ↦ (trajContent κ x₀) (A n)) atTop (𝓝 0)

Tactic:
choose a S mS A_eq using A_cyl

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)
⊢ Tendsto (fun n ↦ (trajContent κ x₀) (A n)) atTop (𝓝 0)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
⊢ (κ.withDensity fun a x ↦ ↑(f a x) * g a x) = (κ.withDensity fun a x ↦ ↑(f a x)).withDensity g

Tactic:
ext a : 1
  rw [Kernel.withDensity_apply]
  swap; · fun_prop
  change (Measure.withDensity (κ a) ((fun x ↦ (f a x : ℝ≥0∞)) * (fun x ↦ (g a x : ℝ≥0∞)))) =
      (withDensity (withDensity κ fun a x ↦ f a x) g) a
  rw [withDensity_mul]
  · rw [Kernel.withDensity_apply _ hg, Kernel.withDensity_apply]
    exact measurable_coe_nnreal_ennreal.comp hf
  · fun_prop
  · fun_prop

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

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable fun p ↦ ((∂κ p.1/∂η p.1) p.2).toReal

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

Tactic:
· refine Measurable.ennreal_toReal <| measurable_from_prod_countable_right'
      (fun a ↦ Measure.measurable_rnDeriv (κ a) (η a)) fun a a' c ha'_mem_a ↦ ?_
    have h_eq : ∀ κ : Kernel α γ, κ a' = κ a := fun κ ↦ by
      ext s hs
      exact mem_of_mem_measurableAtom ha'_mem_a
        (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl
    rw [h_eq κ, h_eq η]

Goal state after:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
⊢ Measurable fun p ↦ (κ.map fun a ↦ (a, ())).density η p.1 p.2 univ
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 : ℕ ≃ ι
s : Set ((i : ι) → X i)
hs : s ∈ measurableCylinders X
⊢ (map (⇑(piCongrLeft X e)) (infinitePiNat fun n ↦ μ (e n))) s = (piContent μ) s

Tactic:
obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders s).1 hs

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
⊢ (map (⇑(piCongrLeft X e)) (infinitePiNat fun n ↦ μ (e n))) (cylinder I S) = (piContent μ) (cylinder I S)
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
⊢ ((partialTraj κ a c).map (frestrictLe₂ hbc)) x₀ = (partialTraj κ a b) x₀

Tactic:
partialTraj_map_frestrictLe₂

Goal state after:
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
⊢ (partialTraj κ a b) x₀ = (partialTraj κ a b) x₀
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr
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
hcb : c ≤ b
⊢ (partialTraj κ a b).map (frestrictLe₂ hcb) = partialTraj κ a c

Tactic:
partialTraj_map_frestrictLe₂

Goal state after:
case inr
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
hcb : c ≤ b
⊢ partialTraj κ a c = partialTraj κ a c
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

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

Tactic:
partialTraj_map_frestrictLe₂

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
b c : ℕ
hcb : c ≤ b
⊢ partialTraj κ a c = partialTraj κ a c
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
ι : 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)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
u_inf : Infinite ↑u
⊢ Tendsto (fun n ↦ (piContent fun i ↦ μ ↑i) (B n)) atTop (𝓝 0)

Tactic:
have count_u : Countable u := Set.countable_iUnion (fun n ↦ (s n).countable_toSet)
    obtain ⟨φ, -⟩ := Classical.exists_true_of_nonempty (α := ℕ ≃ u) nonempty_equiv_of_countable
    conv => enter [1]; ext n; rw [← infinitePiNat_map_piCongrLeft _ φ (B_mem n)]
    convert!
      tendsto_measure_iInter_atTop (fun n ↦ (mB n).nullMeasurableSet) B_anti ⟨0, measure_ne_top _ _⟩
    · rw [B_inter, measure_empty]
    · infer_instance

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
⊢ lmarginalPartialTraj κ b c f = f

Tactic:
ext x

Goal state after:
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 : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ lmarginalPartialTraj κ b c f x = f x
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
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)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hbc : b ≤ c
⊢ lmarginalPartialTraj κ b c f = lmarginalPartialTraj κ b c (lmarginalPartialTraj κ c d f)

Tactic:
hf.lmarginalPartialTraj_of_le d mf hac

Goal state after:
case inl
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)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hbc : b ≤ c
⊢ lmarginalPartialTraj κ b c f = lmarginalPartialTraj κ b c f
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this : ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
a : α
ha : (κ.singularPart η) a = 0
⊢ κ a ≪ η a

Tactic:
rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha

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

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
s : Set (α × β)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β) in Prod.mk a ⁻¹' s, f a b ∂κ a = ∫⁻ (b : β), s.indicator (fun a ↦ f a.1 a.2) (a, b) ∂κ a

Tactic:
← lintegral_indicator (measurable_prodMk_left hs)

Goal state after:
case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
s : Set (α × β)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (a_1 : β), (Prod.mk a ⁻¹' s).indicator (f a) a_1 ∂κ a = ∫⁻ (b : β), s.indicator (fun a ↦ f a.1 a.2) (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ deterministic (fun a ↦ (f a, f a)) ⋯ = deterministic Function.diag ⋯ ∘ₖ deterministic f hf

Tactic:
deterministic_comp_deterministic,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ deterministic (fun a ↦ (f a, f a)) ⋯ = deterministic (Function.diag ∘ f) ⋯
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)
s : Finset ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
⊢ (↑s).pi t = cylinder s (Set.univ.pi fun i ↦ t ↑i)

Tactic:
ext x

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
x : (i : ι) → X i
⊢ x ∈ (↑s).pi t ↔ x ∈ cylinder s (Set.univ.pi fun i ↦ t ↑i)
Module: Mathlib.Probability.Kernel.CompProdEqIff

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
s : Set (α × β)
hs : MeasurableSet s
x✝ : (μ ⊗ₘ η) s < ∞
⊢ (μ ⊗ₘ κ) s = (μ ⊗ₘ η) s

Tactic:
by rw [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
f : α → β
hf : ∀ (a : α), κ a = Measure.dirac (f a)
s : Set β
hs : MeasurableSet s
⊢ {x | f x ∈ s} = {x | s.indicator 1 (f x) = 1}

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
f : α → β
hf : ∀ (a : α), κ a = Measure.dirac (f a)
s : Set β
hs : MeasurableSet s
x : α
⊢ x ∈ {x | f x ∈ s} ↔ x ∈ {x | s.indicator 1 (f x) = 1}
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 : ℕ
⊢ (traj κ a).map (frestrictLe b) = partialTraj κ a b

Tactic:
ext x

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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
s✝ : Set ((i : ↥(Iic b)) → X ↑i)
a✝ : MeasurableSet s✝
⊢ (((traj κ a).map (frestrictLe b)) x) s✝ = ((partialTraj κ a b) x) s✝
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)
Y : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (fun x i ↦ f i (x i)) ⁻¹' (↑s).pi t = (↑s).pi fun i ↦ f i ⁻¹' t i

Tactic:
ext x

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
Y : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
x : (i : ι) → X i
⊢ x ∈ (fun x i ↦ f i (x i)) ⁻¹' (↑s).pi t ↔ x ∈ (↑s).pi fun i ↦ f i ⁻¹' t i