mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun m ↦ ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 0)

Tactic:
by

Goal state after:
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))
a b : ℕ
⊢ IsSFiniteKernel (partialTraj κ a b)

Tactic:
by

Goal state after:
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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
⊢ IsFiniteKernel (partialTraj κ a b)

Tactic:
by

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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂ν a, Tendsto (fun m ↦ κ.density ν a x (seq m)) atTop (𝓝 0)

Tactic:
by

Goal state after:
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 : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
⊢ IsZeroOrMarkovKernel (partialTraj κ a b)

Tactic:
by

Goal state after:
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)) μ)
⊢ μ[fun a ↦ f (X a, Y a) | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a ↦ ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)

Tactic:
by

Goal state after:
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 : AEStronglyMeasurable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)

Tactic:
by

Goal state after:
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 : StronglyMeasurable f
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)

Tactic:
by

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
⊢ countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}

Tactic:
by

Goal state after:
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)
a b : ℕ
⊢ IsMarkovKernel (partialTraj κ a b)

Tactic:
by

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 : γ
⊢ κ.densityProcess κ.fst n a x univ = if (κ.fst a) (countablePartitionSet n x) = 0 then 0 else 1

Tactic:
by

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))
a : ℕ
⊢ partialTraj κ a (a + 1) = (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).map (_root_.IicProdIoc a (a + 1))

Tactic:
by

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 | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}

Tactic:
by

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))
hab : a ≤ b
⊢ partialTraj κ a (b + 1) = partialTraj κ b (b + 1) ∘ₖ partialTraj κ a b

Tactic:
by

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}
⊢ {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u

Tactic:
by

Goal state after:
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))
hab : a ≤ b
hbc : b ≤ c
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c

Tactic:
by

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

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)

Tactic:
by

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst✝ : IsSFiniteKernel η
⊢ deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) = Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ))

Tactic:
by

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

Goal state before:
pp: β : 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 μ
⊢ Integrable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)

Tactic:
by

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 : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x univ = 1

Tactic:
by

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 : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
⊢ _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc

Tactic:
by

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
this : (κ a) (countablePartitionSet n x ×ˢ univ) = 0
⊢ 0 = (κ a) (countablePartitionSet n x ×ˢ univ) / 0

Tactic:
by

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
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ a) {p | p.1 ∈ countablePartitionSet n x}) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}))

Tactic:
by

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
⊢ Tendsto (fun m ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))

Tactic:
by

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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ ∀ᵐ (x : γ) ∂κ.fst a, Tendsto (fun m ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)

Tactic:
by

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 κ
a : α
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
a b : ℕ
h : a = b
⊢ ((i : ↥(Iic a)) → X ↑i) = ((i : ↥(Iic b)) → X ↑i)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
s t : Set ℕ
h : s = t
x : (i : ↑s) → X ↑i
i : ↑t
⊢ cast ⋯ x i = x ⟨↑i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
h : a = b
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
⊢ Measure.map (cast ⋯) (μ a) = μ b

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
h : a = b
⊢ inferInstance ≍ inferInstance

Tactic:
by

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 κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂κ.fst a, Tendsto (fun m ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
u : Set ι
⊢ setBer(u, 0) = dirac ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
u : Set ι
⊢ setBer(u, 1) = dirac u

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ setBer(u, p) ({s | i ∈ s} ∩ {s | i ∉ u}) = setBer(u, p) {s | i ∈ s}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ setBer(u, p) {s | i ∈ s} =
    (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) (cylinder {i} {fun x ↦ True})

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) (cylinder {i} {fun x ↦ True}) = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
⊢ ∀ᵐ (s : Set ι) ∂setBer(u, p), s ⊆ u

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
⊢ frestrictLe a (iterateInduction x ind) = x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
u : Set ι
inst✝ : Countable ι
s : Set ι
p : ↑I
hs : ¬s ⊆ u
⊢ {s} ⊆ {x | (fun s ↦ s ⊆ u) x}ᶜ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
S : Set (Set ι)
⊢ {s | s ∈ S ∧ s ⊆ u} ⊆ S

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
S : Set (Set ι)
⊢ S \ {s | s ∈ S ∧ s ⊆ u} ⊆ {x | (fun s ↦ s ⊆ u) x}ᶜ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
S : Set (Set ι)
⊢ setBer(u, p) S = setBer(u, p) {s | s ∈ S ∧ s ⊆ u}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ Measurable Set.ncard

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ (map Set.ncard setBer(u, p)) s = setBer(u, p) {t | t ⊆ u ∧ t.ncard ∈ s}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ setBer(↑u, p) {s} =
    ∏' (i : ι), ((if i ∈ u ↔ i ∈ s then ↑(toNNReal p) else 0) + if i ∈ s then 0 else ↑(toNNReal (σ p)))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∏' (i : ι), ((if i ∈ u ↔ i ∈ s then ↑(toNNReal p) else 0) + if i ∈ s then 0 else ↑(toNNReal (σ p))) =
    ∏ i ∈ u, if i ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ (∏ i ∈ u, if i ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))) =
    ↑(toNNReal p) ^ s.ncard * ↑(toNNReal (σ p)) ^ (↑u \ s).ncard

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s u : Set ι
p : ↑I
inst✝ : Countable ι
hsu : s ⊆ u
hu : u.Finite
⊢ setBer(u, p) {s} = ↑(toNNReal p) ^ s.ncard * ↑(toNNReal (σ p)) ^ (u \ s).ncard

Tactic:
by

Goal state after:
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)
a : ℕ
⊢ IsProjectiveLimit ν μ ↔ ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s u : Set ι
inst✝ : Countable ι
p : ↑I
hsu : s ⊆ u
hu : u.Finite
⊢ setBer(u, p).real {s} = ↑p ^ s.ncard * (1 - ↑p) ^ (u \ s).ncard

Tactic:
by

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 : ℕ
⊢ {s | s ⊆ u ∧ s.ncard ∈ {k}} ⊆ {b | b ⊆ u}

Tactic:
by

Goal state after:
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)
⊢ IsProjectiveLimit ν μ ↔ ∀ (n : ℕ), Measure.map (frestrictLe n) ν = μ (Iic n)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), SFinite (μ n)
I : Finset ℕ
⊢ SFinite (inducedFamily μ I)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsFiniteMeasure (μ n)
I : Finset ℕ
⊢ IsFiniteMeasure (inducedFamily μ I)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsZeroOrProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsZeroOrProbabilityMeasure (inducedFamily μ I)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsProbabilityMeasure (inducedFamily μ I)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
n : ℕ
x : (i : ↥(Iic ((Iic n).sup id))) → X ↑i
i : ↥(Iic n)
⊢ ↑(Iic ((Iic n).sup id)) = ↑(Iic n)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
n : ℕ
⊢ inducedFamily μ (Iic n) = μ n

Tactic:
by

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:
by

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:
by

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
s : Set ι
hs : s ∈ this.toFinset
⊢ setBer(u, p).real {s} = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
⊢ IsProjectiveMeasureFamily (inducedFamily μ)

Tactic:
by

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 : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ (trajContent κ x₀) (cylinder (Iic b) S) = ((partialTraj κ a b) x₀) S

Tactic:
by

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)).real {k} = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
by

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:
by

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} = ENNReal.ofReal (↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k))

Tactic:
by

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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ (trajContent κ (frestrictLe a x₀)) (cylinder (Iic b) S) =
    lmarginalPartialTraj κ a b ((cylinder (Iic b) S).indicator 1) x₀

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∈ s
⊢ {t | t ∈ s ∧ t ⊆ ∅} = {∅}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
⊢ {t | t ∈ s ∧ t ⊆ ∅} = ∅

Tactic:
by

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)
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)
n : ℕ
⊢ Nonempty (X n)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
p : ↑I
inst✝ : Countable ι
⊢ setBer(∅, p) = dirac ∅

Tactic:
by

Goal state after: