mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : ¬IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

Tactic:
·

Goal state after:
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : ¬IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' Prod.snd ⁻¹' s) ∂μ = ∫⁻ (a : α), (κ a) s ∂μ

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' Prod.snd ⁻¹' s) ∂μ = ∫⁻ (a : α), (κ a) s ∂μ
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

Tactic:
·

Goal state after:
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : ¬IsSFiniteKernel κ
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : ¬IsSFiniteKernel κ
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂η x ∂κ x = ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂κ x ∂η x

Tactic:
·

Goal state after:
case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ ∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ×ₖ κ) ∘ₘ μ

Tactic:
compProd,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = ⇑(Kernel.id ×ₖ κ) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : ¬IsSFiniteKernel κ
⊢ ⇑η ∘ₘ μ ⊗ₘ κ = (⇑(κ ⊗ₖ η) ∘ₘ μ).snd

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ ⇑η ∘ₘ μ ⊗ₘ κ = (⇑(κ ⊗ₖ η) ∘ₘ μ).snd

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : ¬IsSFiniteKernel κ
⊢ ⇑η ∘ₘ μ ⊗ₘ κ = (⇑(κ ⊗ₖ η) ∘ₘ μ).snd
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' {a | ¬p a})) =ᵐ[κ a] 0

pp: case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ MeasurableSet {a | ¬p a}

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' {a | ¬p a})) =ᵐ[κ a] 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ MeasurableSet {a | ¬p a}

Tactic:
·

Goal state after:
case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ MeasurableSet {a | ¬p a}
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (b : β), (η (a, b)) s ∂κ a ∂μ = ∫⁻ (a : α), ((κ ⊗ₖ η) a) (Prod.snd ⁻¹' s) ∂μ

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: case pos.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) s ∂κ a = ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a

pp: case pos.e_f.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
·

Goal state after:
case pos.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) s ∂κ a = ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: case pos.e_f.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
·

Goal state after:
case pos.e_f.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∈ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = (η (a, b)) ({c | (b, c) ∈ u} ∩ t)

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∉ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∈ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = (η (a, b)) ({c | (b, c) ∈ u} ∩ t)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∉ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
h : b ∉ s
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = 0
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : ¬CompleteSpace E
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f y ∂κ x

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f y ∂κ x

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : ¬CompleteSpace E
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f y ∂κ x
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a✝ : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ ∀ (n : ℕ), Measurable fun c ↦ (F n) (a, c)

pp: case h_mono
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a✝ : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ Monotone fun n c ↦ (F n) (a, c)

Tactic:
·

Goal state after:
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a✝ : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ ∀ (n : ℕ), Measurable fun c ↦ (F n) (a, c)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case h_mono
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a✝ : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ Monotone fun n c ↦ (F n) (a, c)

Tactic:
·

Goal state after:
case h_mono
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a✝ : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ Monotone fun n c ↦ (F n) (a, c)
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case pos.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
n : ℕ
⊢ StronglyMeasurable (f' n)

pp: case pos.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
⊢ Tendsto f' atTop (𝓝 fun x ↦ ∫ (y : β), f y ∂κ x)

Tactic:
·

Goal state after:
case pos.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
n : ℕ
⊢ StronglyMeasurable (f' n)
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case pos.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
⊢ Tendsto f' atTop (𝓝 fun x ↦ ∫ (y : β), f y ∂κ x)

Tactic:
·

Goal state after:
case pos.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
⊢ Tendsto f' atTop (𝓝 fun x ↦ ∫ (y : β), f y ∂κ x)
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
x : α
hfx : Integrable f (κ x)
⊢ Tendsto (fun i ↦ f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
x : α
hfx : ¬Integrable f (κ x)
⊢ Tendsto (fun i ↦ f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
x : α
hfx : Integrable f (κ x)
⊢ Tendsto (fun i ↦ f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))