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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
⊢ ((if i = 0 then κ else 0) a) s = if i = 0 then (κ a) s else 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
⊢ ((if i = 0 then κ else 0) a) s = if i = 0 then (κ a) s else 0
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic id ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic id ⋯)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic Function.diag ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic Function.diag ⋯)
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
h : ∀ i ∈ ∅, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel 0

Tactic:
;

Goal state after:
case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
h : ∀ i ∈ ∅, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel 0
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
⊢ #{i | ¬f i (x i) = f i (y i)} ≤ #{i | ¬x i = y i}

Tactic:
;

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
⊢ #{i | ¬f i (x i) = f i (y i)} ≤ #{i | ¬x i = y i}
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
i : ι
a✝ : i ∈ univ
⊢ x i = y i → f i (x i) = f i (y i)

Tactic:
;

Goal state after:
case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
i : ι
a✝ : i ∈ univ
⊢ x i = y i → f i (x i) = f i (y i)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic (fun x ↦ PUnit.unit) ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic (fun x ↦ PUnit.unit) ⋯)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic Prod.swap ⋯)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic Prod.swap ⋯)
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ #{i | ¬x i = y i} ≤ #{i | ¬f i (x i) = f i (y i)}

Tactic:
;

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ #{i | ¬x i = y i} ≤ #{i | ¬f i (x i) = f i (y i)}
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
i : ι
a✝ : i ∈ univ
⊢ f i (x i) = f i (y i) → x i = y i

Tactic:
;

Goal state after:
case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
i : ι
a✝ : i ∈ univ
⊢ f i (x i) = f i (y i) → x i = y i
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
x : α
s : Set β
a✝ : MeasurableSet s
⊢ ((const α 0) x) s = (0 x) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
x : α
s : Set β
a✝ : MeasurableSet s
⊢ ((const α 0) x) s = (0 x) s
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst✝ : MeasurableSpace β
μ ν : Measure α
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((const β (μ + ν)) a✝¹) s✝ = ((const β μ + const β ν) a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst✝ : MeasurableSpace β
μ ν : Measure α
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((const β (μ + ν)) a✝¹) s✝ = ((const β μ + const β ν) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
inst✝ : SFinite μβ
⊢ const α μβ = const α (Measure.sum (sfiniteSeq μβ))

Tactic:
sum_sfiniteSeq

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
inst✝ : SFinite μβ
⊢ const α μβ = const α μβ
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ ((κ.comapRight ⋯) a✝) s✝ = (κ a✝) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ ((κ.comapRight ⋯) a✝) s✝ = (κ a✝) s✝
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ (κ a✝) (id '' s✝) = (κ a✝) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ (κ a✝) (id '' s✝) = (κ a✝) s✝
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 : ι) → AddGroup (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (ofHamming x) (ofHamming y)) = ↑(hammingNorm (ofHamming (-x + y)))

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (ofHamming x) (ofHamming y)) = ↑(hammingNorm (ofHamming (-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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (κ.comapRight hf) a = (Kernel.sum fun n ↦ (κ.seq n).comapRight hf) a

Tactic:
rw [sum_apply]

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.Composition.Comp

Goal state before:

Tactic:
∫⁻ b, η b Set.univ ∂κ a ≤ ∫⁻ _, Cη ∂κ a :=
      lintegral_mono fun b => measure_le_bound η b Set.univ
    _ = Cη * κ a Set.univ := MeasureTheory.lintegral_const Cη
    _ = κ a Set.univ * Cη := mul_comm _ _

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 γ
κ : Kernel α β
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((0 ∘ₖ κ) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((0 ∘ₖ κ) a✝¹) s✝ = (0 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 β γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ∘ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ∘ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝
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 : α
t : Set β
⊢ (if a ∈ s then κ a else η a) t = if a ∈ s then (κ a) t else (η a) t

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 : α
t : Set β
⊢ (if a ∈ s then κ a else η a) t = if a ∈ s then (κ a) t else (η 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∞
⊢ (∫⁻ (b : β), g b ∂if a ∈ s then κ a else η 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 ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η 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∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then κ a else η 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 ∂if a ∈ s then κ a else η a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set PUnit.{u_4 + 1}
a✝ : MeasurableSet s✝
⊢ ((discard β ∘ₖ κ) a✝¹) s✝ = ((discard α) a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set PUnit.{u_4 + 1}
a✝ : MeasurableSet s✝
⊢ ((discard β ∘ₖ κ) a✝¹) s✝ = ((discard α) a✝¹) s✝
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
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc r (r * maxLen)
D : ℝ := ↑(Fintype.card α)
w : Fin r → ↥S
⊢ ∏ i, (1 / D) ^ (↑(w i)).length = (1 / D) ^ (concatFn w).length

Tactic:
simpa [concatFn_length] using Finset.prod_pow_eq_pow_sum Finset.univ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
h' : sᶜ = ∅
⊢ μ = 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
h' : sᶜ = ∅
⊢ μ = 0
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.Composition.Comp

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a : α
⊢ (κ a) Set.univ ≤ κ.bound

Tactic:
;

Goal state after:
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a : α
⊢ (κ a) Set.univ ≤ κ.bound
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
m n : ℕ
a : α
s : Set α
hs : MeasurableSet s
⊢ ((κ ^ (n + m)) a) s = ∫⁻ (b : α), ((κ ^ n) b) s ∂(κ ^ m) a

Tactic:
;

Goal state after:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
m n : ℕ
a : α
s : Set α
hs : MeasurableSet s
⊢ ((κ ^ (n + m)) a) s = ∫⁻ (b : α), ((κ ^ n) b) s ∂(κ ^ m) 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 a ↦ ∫⁻ (b : β), f a b ∂(κ.restrict hs) 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 : β), f a b ∂(κ.restrict hs) 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 : β), f a b ∂(κ.restrict hs) 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 : β), f a b ∂(κ.restrict hs) b
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : IsSFiniteKernel η
a✝¹ : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((0 ∥ₖ η) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
;

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : IsSFiniteKernel η
a✝¹ : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((0 ∥ₖ η) a✝¹) s✝ = (0 a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
a✝¹ : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((κ ∥ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
;

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
a✝¹ : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((κ ∥ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos.inl
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
f : β → γ
hf : Measurable f
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0

Tactic:
;

Goal state after:
case pos.inl
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
f : β → γ
hf : Measurable f
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos.inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
h : IsMarkovKernel κ
this : IsMarkovKernel (κ.map f)
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
;

Goal state after:
case pos.inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
h : IsMarkovKernel κ
this : IsMarkovKernel (κ.map f)
⊢ IsZeroOrMarkovKernel (κ.map f)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel 0

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel 0
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
a✝¹ : γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((comap 0 g hg) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
a✝¹ : γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((comap 0 g hg) a✝¹) s✝ = (0 a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.comap id ⋯) a✝¹) s✝ = (κ a✝¹) s✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.comap id ⋯) a✝¹) s✝ = (κ a✝¹) s✝