mathlib-initiative/mathlib-tactics huggingface dataset:
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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
by

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 b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i

Tactic:
by

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 b : ι
hab : a ≤ b
⊢ Measurable
    ⇑{ toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }

Tactic:
by

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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable X (Measure.map Prod.snd (ν.prod μ))

Tactic:
by

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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable Y (Measure.map Prod.snd (ν.prod μ))

Tactic:
by

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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable Prod.snd (ν.prod μ)

Tactic:
by

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 : ((i : ↥(Iic a)) → X ↑i) × ((i : ↑(Set.Ioi a)) → X ↑i)
⊢ (fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i)) ((fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩) x) = x

Tactic:
by

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

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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  ⇑(condDistrib Y X (Measure.map Prod.snd (ν.prod μ))) =ᵐ[Measure.map (X ∘ Prod.snd) (ν.prod μ)]
    ⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ))
⊢ AEMeasurable X (Measure.map Prod.snd (ν.prod μ))

Tactic:
by

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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  ⇑(condDistrib Y X (Measure.map Prod.snd (ν.prod μ))) =ᵐ[Measure.map (X ∘ Prod.snd) (ν.prod μ)]
    ⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ))
⊢ AEMeasurable Prod.snd (ν.prod μ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
⊢ ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
this : ⇑κ =ᵐ[(μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel
⊢ ⇑(μ ⊗ₘ κ).condKernel =ᵐ[μ] ⇑κ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ ⇑(μ ⊗ₘ κ).condKernel =ᵐ[μ] ⇑κ

Tactic:
by

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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
by

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 : ι
⊢ Measurable
    ⇑{ toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
⊢ Measurable ⇑{ toFun := fun x i ↦ ⋯ ▸ x, invFun := fun x ↦ x ⟨a + 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Tactic:
by

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 : AEMeasurable X μ
hs : MeasurableSet s
⊢ Integrable (fun a ↦ ((condDistrib Y X μ) (X a)).real s) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b ↦ (a, b)) ⋯

Tactic:
by

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

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
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂Measure.map X μ, Integrable (fun ω ↦ f (b, ω)) ((condDistrib Y X μ) b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ (fun b ↦ κ (a, b)) =ᵐ[ρ.fst a] ⇑(ρ a).condKernel

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
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ Integrable (fun x ↦ ∫ (y : Ω), ‖f (x, y)‖ ∂(condDistrib Y X μ) x) (Measure.map X μ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel

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
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ Integrable (fun x ↦ ‖∫ (y : Ω), f (x, y) ∂(condDistrib Y X μ) x‖) (Measure.map 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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)

Tactic:
by

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 Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in X ⁻¹' t, ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s)

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ ∀ᵐ (x : β) ∂ρ.fst a, κ (a, x) = ρ.condKernel (a, x)

Tactic:
by

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

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))
hba : b ≤ a
⊢ partialTraj κ a b = deterministic (frestrictLe₂ hba) ⋯

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 = Kernel.id

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 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
⊢ partialTraj κ a 0 = deterministic (frestrictLe₂ ⋯) ⋯

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 =
    Nat.leRec Kernel.id
      (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) hab

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun x ↦ (κ x).real s) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[κ a] g a
⊢ ∫ (a : α), ∫ (b : β), f a b ∂κ a ∂μ = ∫ (a : α), ∫ (b : β), g a b ∂κ a ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a

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
⊢ ¬b + 1 ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
a : α
inst✝ : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
⊢ ∫ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : β → E
a : α
inst✝¹ : CompleteSpace E
g : α → β
inst✝ : MeasurableSingletonClass β
hg : Measurable g
⊢ ∫ (x : β), f x ∂(deterministic g hg) a = f (g 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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ ∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (A ×ˢ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : β → E
a : α
inst✝¹ : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ), ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : β → E
a : α
inst✝² : CompleteSpace E
g : α → β
inst✝¹ : MeasurableSingletonClass β
hg : Measurable g
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
⊢ ∫ (x : β), f x ∂(const α μ) a = ∫ (x : β), f x ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
s : Set β
⊢ ∫ (x : β) in s, f x ∂(const α μ) a = ∫ (x : β) in s, f x ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫ (x : β), f x ∂(κ.restrict hs) a = ∫ (x : β) in s, f x ∂κ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
⊢ ∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a

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) =
    (Kernel.id ×ₖ (κ b).map ⇑(piSingleton b) ∘ₖ partialTraj κ a b).map (_root_.IicProdIoc b (b + 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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun m ↦ ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 ((κ a).real univ))

Tactic:
by

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 : Measurable Y
hs : MeasurableSet s
⊢ (fun a ↦ ((condDistrib Y X μ) (X a)).real s) =ᵐ[μ] μ[(Y ⁻¹' s).indicator fun ω ↦ 1 | MeasurableSpace.comap X mβ]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
⊢ ∫ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
t : Set β
⊢ ∫ (b : β) in t, g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η 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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto (fun m ↦ (κ a) (univ ×ˢ seq m)) atTop (𝓝 ((κ a) (⋂ n, (fun m ↦ univ ×ˢ seq m) n)))

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
κ : Kernel X Y
μ : Measure X
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂κ x ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂κ x ∂μ

Tactic:
by

Goal state after: