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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((κ.comapRight hf) a) t = (κ a) (f '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comapRight ⋯ = κ

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ (Bornology.cobounded (Hamming β)).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
⊢ IsMarkovKernel (κ.comapRight hf)

Tactic:
by

Goal state after:
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 β), dist x y = ‖-x + y‖

Tactic:
by

Goal state after:
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✝ : IsFiniteKernel κ
hf : MeasurableEmbedding f
⊢ IsFiniteKernel (κ.comapRight hf)

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ (fun a ↦ (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a ↦ (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
⊢ (concatFn w).length = ∑ i, (↑(w i)).length

Tactic:
by

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 β γ
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((η ∘ₖ κ) a) s = ∫⁻ (b : β), (η b) s ∂κ a

Tactic:
by

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 α β
η : Kernel β γ
a : α
⊢ ((η ∘ₖ κ) a) Set.univ ≤ (κ a) Set.univ * η.bound

Tactic:
by

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 α β
⊢ 0 ∘ₖ κ = 0

Tactic:
by

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 β γ
⊢ κ ∘ₖ 0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ Kernel.id ∘ₖ κ = κ

Tactic:
by

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
⊢ κ ∘ₖ Kernel.id = κ

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ ∀ w ∈ List.ofFn fun i ↦ ↑(w₁ i), w ∈ ↑S

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ ∀ w ∈ List.ofFn fun i ↦ ↑(w₂ i), w ∈ ↑S

Tactic:
by

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 α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η b) (toMeasurable ((η ∘ₖ κ) a) s) < ∞

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
⊢ Function.Injective concatFn

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
x : List α
hx : x ∈ {x ∈ T | x.length = s}
⊢ (1 / ↑(Fintype.card α)) ^ x.length = (1 / ↑(Fintype.card α)) ^ s

Tactic:
by

Goal state after:
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 : α
⊢ (Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)) = Measure.comap f (Measure.sum fun n ↦ (κ.seq n) a)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ ∑ x ∈ T with x.length = s, (1 / ↑(Fintype.card α)) ^ s = ↑{x ∈ T | x.length = s}.card * (1 / ↑(Fintype.card α)) ^ s

Tactic:
by

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 α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η b) s < ∞

Tactic:
by

Goal state after:
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
⊢ IsSFiniteKernel (κ.comapRight hf)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ ∑ x ∈ T with x.length = s, (1 / ↑(Fintype.card α)) ^ x.length ≤ ↑(Fintype.card α) ^ s * (1 / ↑(Fintype.card α)) ^ s

Tactic:
by

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 α β
η : Kernel β γ
s : Set γ
a : α
hs : MeasurableSet s
⊢ ((η ∘ₖ κ) a) s = 0 ↔ (fun y ↦ (η y) s) =ᵐ[κ a] 0

Tactic:
by

Goal state after:
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 β
⊢ ((piecewise hs κ η) a) t = if a ∈ s then (κ a) t else (η a) t

Tactic:
by

Goal state after:
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✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (Kernel.piecewise hs κ η)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
i : Fin r
x✝ : i ∈ Finset.univ
⊢ 1 ≤ (↑(w i)).length

Tactic:
by

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 α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
⊢ (fun x ↦ (η x) s) =ᵐ[κ a] 0

Tactic:
by

Goal state after:
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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (Kernel.piecewise hs κ η)

Tactic:
by

Goal state after:
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 η
⊢ IsSFiniteKernel (piecewise hs κ η)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ ∑ i, S.sup List.length = r * S.sup List.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' f i)
a : α
⊢ (κ a) (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), (κ a) (Prod.mk a ⁻¹' f i)

Tactic:
by

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 α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z
⊢ ∀ᵐ (z : γ) ∂(η ∘ₖ κ) a, p z

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ (concatFn w).length ∈ Finset.Icc r (r * S.sup List.length)

Tactic:
by

Goal state after:
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:
by

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 α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
⊢ η.restrict hs ∘ₖ κ = (η ∘ₖ κ).restrict hs

Tactic:
by

Goal state after:
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
w✝ : Fin r → ↥S
left✝ : w✝ ∈ Finset.univ
hx : concatFn w✝ ∈ T
c : ↥S
hnil : ↑c = []
⊢ [] ∈ ↑S

Tactic:
by

Goal state after:
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:
by

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 β γ
κ : Kernel α β
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂(η ∘ₖ κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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 α β
⊢ ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ discard β ∘ₖ κ = { toFun := fun a ↦ (κ a) Set.univ • Measure.dirac PUnit.unit, measurable' := ⋯ }

Tactic:
by

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)
h' : μ ≠ 0
⊢ μ (toMeasurable μ {a | ¬IsProbabilityMeasure (κ a)}) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ discard β ∘ₖ κ = discard α

Tactic:
by

Goal state after:
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 ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r = ∑ w, ∏ i, (1 / D) ^ (↑(w i)).length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
⊢ swap α α ∘ₖ copy α = copy α

Tactic:
by

Goal state after:
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
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)

Tactic:
by

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)
h' : μ ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s = 0 ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a)

Tactic:
by

Goal state after:
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, ∏ i, (1 / D) ^ (↑(w i)).length = ∑ w, (1 / D) ^ (concatFn w).length

Tactic:
by

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 γ
μ : Measure γ
κ : Kernel α β
⊢ ⇑(const β μ ∘ₖ κ) = fun a ↦ (κ a) Set.univ • μ

Tactic:
by

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)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
⊢ sᶜ.Nonempty

Tactic:
by

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 γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ const β μ ∘ₖ κ = const α μ

Tactic:
by

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 α β
η : Kernel β γ
⊢ η ∘ₖ (μ + κ) = η ∘ₖ μ + η ∘ₖ κ

Tactic:
by

Goal state after:
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 : α
⊢ Measurable fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
by

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 α β
κ η : Kernel β γ
⊢ (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ

Tactic:
by

Goal state after:
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 (Function.const (α × β) c) (a, b) ∂κ a

Tactic:
by

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
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∑' (i : ι), ∫⁻ (b : β), (η b) s✝ ∂(κ i) a✝ = ∑' (i : ι), ((η ∘ₖ κ i) a✝) s✝

Tactic:
comp_apply' _ _ _ hs

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
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
⊢ η ∘ₖ Kernel.sum κ = Kernel.sum fun i ↦ η ∘ₖ κ i

Tactic:
by

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
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∫⁻ (b : β), ∑' (i : ι), ((η i) b) s✝ ∂κ a✝ = ∑' (i : ι), ((η i ∘ₖ κ) a✝) s✝

Tactic:
comp_apply' _ _ _ hs

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✝
⊢ ∫⁻ (b : β), ∑' (i : ι), ((η i) b) s✝ ∂κ a✝ = ∑' (i : ι), ∫⁻ (b : β), ((η i) b) s✝ ∂κ a✝
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)
h' : μ ≠ 0
⊢ ∃ η, ⇑κ =ᵐ[μ] ⇑η ∧ IsMarkovKernel η

Tactic:
by

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
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
⊢ Kernel.sum η ∘ₖ κ = Kernel.sum fun i ↦ η i ∘ₖ κ

Tactic:
by

Goal state after:
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✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
b : Bool
⊢ ((boolKernel μ ν) b) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

Tactic:
by

Goal state after:
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 : β), s.indicator 1 b * t.indicator 1 b ∂κ a = ∫⁻ (b : β), (s ∩ t).indicator 1 b ∂κ a

Tactic:
by

Goal state after:
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
⊢ ((copy β ∘ₖ κ) a) (s ×ˢ t) = (κ a) (s ∩ t)

Tactic:
by

Goal state after:
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✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
b : Bool
⊢ IsProbabilityMeasure ((boolKernel μ ν) b)

Tactic:
by

Goal state after:
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 μ
inst✝ : SFinite ν
⊢ ∃ κs, (∀ (n : ℕ), IsFiniteKernel (κs n)) ∧ boolKernel μ ν = Kernel.sum κs

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
⊢ κ = boolKernel (κ false) (κ true)

Tactic:
by

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 β γ
inst✝¹ : IsMarkovKernel η
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
⊢ IsProbabilityMeasure ((η ∘ₖ κ) a)

Tactic:
by

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 γ
inst✝¹ : IsZeroOrMarkovKernel 0
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel 0

Tactic:
by

Goal state after:
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
⊢ (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r ≤ ↑r * ↑(S.sup List.length)

Tactic:
by

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

Goal state before:
pp: case h_mono
α : 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
a : α
⊢ Monotone fun n b ↦ (F n) (a, b)

Tactic:
· exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _

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 β γ
inst✝¹ : IsZeroOrMarkovKernel η
inst✝ : IsZeroOrMarkovKernel 0
h✝ : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel 0

Tactic:
by

Goal state after: