mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
hk : ∀ (i : ι), IsSMulRegular (β i) k
x : (i : ι) → β i
i : ι
⊢ k • 0 = 0

Tactic:
[

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
hk : ∀ (i : ι), IsSMulRegular (β i) k
x : (i : ι) → β i
i : ι
⊢ k • 0 = 0
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (-x + y)

Tactic:
[

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (-x + y)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t✝ : Set β
κ : Kernel α β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable fun b ↦ ((κ b).restrict s) t

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t✝ : Set β
κ : Kernel α β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable fun b ↦ ((κ b).restrict s) t
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (κ.restrict hs) a = (Kernel.sum fun n ↦ (κ.seq n).restrict hs) a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (κ.restrict hs) a = (Kernel.sum fun n ↦ (κ.seq n).restrict hs) a
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)

Tactic:
[

Goal state after:
case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' tᶜ)

Tactic:
[

Goal state after:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' tᶜ)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this : (fun a ↦ (Measure.comap f (κ a)) t) = fun a ↦ (κ a) (f '' t)
⊢ Measurable fun b ↦ (Measure.comap f (κ b)) t

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this : (fun a ↦ (Measure.comap f (κ a)) t) = fun a ↦ (κ a) (f '' t)
⊢ Measurable fun a ↦ (κ a) (f '' t)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (κ.comapRight hf) a = Measure.sum fun n ↦ ((κ.seq n).comapRight hf) a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (κ.comapRight hf) a = Measure.sum fun n ↦ ((κ.seq n).comapRight hf) a
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this : (fun a ↦ (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a ↦ (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ (κ a) (univ \ Prod.mk a ⁻¹' t)

Tactic:
this

Goal state after:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this : (fun a ↦ (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a ↦ (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : ((η ∘ₖ κ) a) t = 0
⊢ (fun x ↦ (η x) s) =ᵐ[κ a] 0

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : ((η ∘ₖ κ) a) t = 0
⊢ (fun x ↦ (η x) s) =ᵐ[κ a] 0
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (piecewise hs κ η) a = (Kernel.sum fun n ↦ piecewise hs (κ.seq n) (η.seq n)) a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (piecewise hs κ η) a = (Kernel.sum fun n ↦ piecewise hs (κ.seq n) (η.seq n)) a
Module: Mathlib.Probability.Kernel.Basic

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

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
⊢ ∫⁻ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((η.restrict hs ∘ₖ κ) a) t = (((η ∘ₖ κ).restrict hs) a) t

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((η.restrict hs ∘ₖ κ) a) t = (((η ∘ₖ κ).restrict hs) a) t
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
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:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
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
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image concatFn Finset.univ
x : List α
hx : x ∈ T
⊢ x.length ∈ Finset.Icc r (r * maxLen)

Tactic:
rcases Finset.mem_image.mp hx with ⟨_, _, rfl⟩

Goal state after:
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image concatFn Finset.univ
w✝ : Fin r → ↥S
left✝ : w✝ ∈ Finset.univ
hx : concatFn w✝ ∈ T
⊢ (concatFn w✝).length ∈ Finset.Icc r (r * maxLen)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂(η ∘ₖ κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a

Tactic:
by
  rw [comp_apply, Measure.lintegral_bind (Kernel.aemeasurable _) hg.aemeasurable]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ)) a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ)) a
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) x✝) s✝ = ((κ x✝) Set.univ • μ) s✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) x✝) s✝ = ((κ x✝) Set.univ • μ) s✝
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
⊢ Measurable fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
⊢ Measurable fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
⊢ Measurable fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
⊢ Measurable fun b ↦ (η (a, b)) {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) a✝¹) s✝ = ((const α μ) a✝¹) s✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) a✝¹) s✝ = ((const α μ) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel β γ
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((κ + η) ∘ₖ μ) a) s = ((κ ∘ₖ μ + η ∘ₖ μ) a) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel β γ
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((κ + η) ∘ₖ μ) a) s = ((κ ∘ₖ μ + η ∘ₖ μ) a) s
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a ↦ ∫⁻ (b : β), t.indicator (fun x ↦ c) (a, b) ∂κ a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a ↦ ∫⁻ (b : β), t.indicator (fun x ↦ c) (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ Kernel.sum κ) a✝) s✝ = ((Kernel.sum fun i ↦ η ∘ₖ κ i) a✝) s✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ Kernel.sum κ) a✝) s✝ = ((Kernel.sum fun i ↦ η ∘ₖ κ i) a✝) s✝
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
⊢ Measurable fun a ↦ ∫⁻ (b : β), f a b ∂κ a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
⊢ Measurable fun a ↦ ∫⁻ (b : β), f a b ∂κ a
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((Kernel.sum η ∘ₖ κ) a✝) s✝ = ((Kernel.sum fun i ↦ η i ∘ₖ κ) a✝) s✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((Kernel.sum η ∘ₖ κ) a✝) s✝ = ((Kernel.sum fun i ↦ η i ∘ₖ κ) a✝) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ((copy β) b) (s ×ˢ t) ∂κ a = (κ a) (s ∩ t)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ((copy β) b) (s ×ˢ t) ∂κ a = (κ a) (s ∩ t)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
⊢ Measurable fun a ↦ ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
⊢ Measurable fun a ↦ ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
⊢ Measurable fun a ↦ ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
⊢ Measurable fun a ↦ ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (η ∘ₖ κ)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (η ∘ₖ κ)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a ↦ ∫⁻ (b : β) in s, f a b ∂κ a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a ↦ ∫⁻ (b : β) in s, f a b ∂κ a
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (a : β) in s, f a b ∂κ b

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (a : β) in s, f a b ∂κ b
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((κ b.1).prod (η b.2)) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((κ b.1).prod (η b.2)) s