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

Goal state before:
pp: case calc.step.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * maxLen)
⊢ ∑ i ∈ Finset.Icc 0 (0 * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑0 * ↑maxLen

pp: case calc.step.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * maxLen)
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑(0 + 1) * ↑maxLen

pp: case calc.step.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * maxLen)
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑maxLen

Tactic:
<;>

Goal state after:
case calc.step.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * maxLen)
⊢ ∑ i ∈ Finset.Icc 0 (0 * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑0 * ↑maxLen

case calc.step.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * maxLen)
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑(0 + 1) * ↑maxLen

case calc.step.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
maxLen : ℕ := S.sup List.length
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * maxLen)
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * maxLen), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑maxLen
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) false) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

pp: case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) true) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) false) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) true) Set.univ ≤ max (μ Set.univ) (ν Set.univ)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ((boolKernel μ ν) false)

pp: case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ((boolKernel μ ν) true)

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ((boolKernel μ ν) false)

case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ((boolKernel μ ν) true)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure μ

pp: case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ν

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure μ

case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ν
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((boolKernel μ ν) false) s✝ = (Measure.sum fun n ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)) false) s✝

pp: case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((boolKernel μ ν) true) s✝ = (Measure.sum fun n ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)) true) s✝

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((boolKernel μ ν) false) s✝ = (Measure.sum fun n ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)) false) s✝

case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((boolKernel μ ν) true) s✝ = (Measure.sum fun n ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)) true) s✝
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case false
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ (κ false) s✝ = ((boolKernel (κ false) (κ true)) false) s✝

pp: case true
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ (κ true) s✝ = ((boolKernel (κ false) (κ true)) true) s✝

Tactic:
<;>

Goal state after:
case false
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ (κ false) s✝ = ((boolKernel (κ false) (κ true)) false) s✝

case true
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ (κ true) s✝ = ((boolKernel (κ false) (κ true)) true) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

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

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst✝ : IsZeroOrMarkovKernel η
h✝ : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsZeroOrMarkovKernel η
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (η ∘ₖ 0)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst✝ : IsZeroOrMarkovKernel η
h✝ : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
hr : True
hlen_maps : ∀ x ∈ T, x.length = r + 1 + 1
⊢ 0 ≤ ↑r + 1

pp: case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hr : True
hlen_maps : ∀ x ∈ T, r + 1 < x.length ∧ x.length ≤ (r + 1 + 1) * (maxLen + 1 + 1)
⊢ ↑((r + 1 + 1) * (maxLen + 1 + 1) - (r + 1)) ≤ (↑r + 1 + 1) * (↑maxLen + 1 + 1)

Tactic:
<;>

Goal state after:
case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
hr : True
hlen_maps : ∀ x ∈ T, x.length = r + 1 + 1
⊢ 0 ≤ ↑r + 1

case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hr : True
hlen_maps : ∀ x ∈ T, r + 1 < x.length ∧ x.length ≤ (r + 1 + 1) * (maxLen + 1 + 1)
⊢ ↑((r + 1 + 1) * (maxLen + 1 + 1) - (r + 1)) ≤ (↑r + 1 + 1) * (↑maxLen + 1 + 1)
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
hr : True
hlen_maps : ∀ x ∈ T, x.length = r + 1 + 1
⊢ 0 ≤ r + 1

pp: case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hr : True
hlen_maps : ∀ x ∈ T, r + 1 < x.length ∧ x.length ≤ (r + 1 + 1) * (maxLen + 1 + 1)
⊢ (r + 1 + 1) * (maxLen + 1 + 1) - (r + 1) ≤ (r + 1 + 1) * (maxLen + 1 + 1)

Tactic:
<;>

Goal state after:
case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
hr : True
hlen_maps : ∀ x ∈ T, x.length = r + 1 + 1
⊢ 0 ≤ r + 1

case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hr : True
hlen_maps : ∀ x ∈ T, r + 1 < x.length ∧ x.length ≤ (r + 1 + 1) * (maxLen + 1 + 1)
⊢ (r + 1 + 1) * (maxLen + 1 + 1) - (r + 1) ≤ (r + 1 + 1) * (maxLen + 1 + 1)
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 κ
η : Kernel β γ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)

Tactic:
by
  obtain rfl | _ := eq_zero_or_isMarkovKernel κ <;> obtain rfl | _ := eq_zero_or_isMarkovKernel η
  all_goals simpa using by infer_instance

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
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ 1 < K

pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ 0 < K

Tactic:
<;>

Goal state after:
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ 1 < K

α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ 0 < K
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 κ
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
have := IsMarkovKernel.map κ hf; infer_instance

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
x : α × γ
inst✝¹ : IsZeroOrMarkovKernel η
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (0 ∥ₖ η)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsZeroOrMarkovKernel κ
inst✝ : IsZeroOrMarkovKernel η
h✝ : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
x : α × γ
inst✝¹ : IsZeroOrMarkovKernel η
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (0 ∥ₖ η)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsZeroOrMarkovKernel κ
inst✝ : IsZeroOrMarkovKernel η
h✝ : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)
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 : α × γ
inst✝¹ : IsZeroOrMarkovKernel κ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)

Tactic:
by
  obtain rfl | _ := eq_zero_or_isMarkovKernel κ <;> obtain rfl | _ := eq_zero_or_isMarkovKernel η
  all_goals simpa using by infer_instance

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

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 α (β × γ)
h : IsFiniteKernel κ.fst
a : α
⊢ (κ a) Set.univ ≤ (κ.fst a) Set.univ

Tactic:
fst_apply' _ _ MeasurableSet.univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
a : α
⊢ (κ a) Set.univ ≤ (κ a) {p | p.1 ∈ Set.univ}
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ((κ ⊗ₖ η) a) (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂μ =
    ∫⁻ (a : α × β), (η a) (Prod.mk a ⁻¹' s) ∂μ ⊗ₘ κ

Tactic:
Measure.lintegral_compProd

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ((κ ⊗ₖ η) a) (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a ∂μ

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ Measurable fun a ↦ (η a) (Prod.mk a ⁻¹' 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 α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∈ s
⊢ (η (a✝, a)) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun b ↦ (η (a✝, b)) t) a

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∉ s
⊢ (η (a✝, a)) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun b ↦ (η (a✝, b)) t) a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∈ s
⊢ (η (a✝, a)) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun b ↦ (η (a✝, b)) t) a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∉ s
⊢ (η (a✝, a)) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun b ↦ (η (a✝, b)) t) a
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
a : α
⊢ ((κ ∥ₖ η).fst ∘ₖ copy α) a = κ a

Tactic:
rw [comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), fst_apply, parallelComp_apply]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
a : α
⊢ Measure.map Prod.fst ((κ (a, a).1).prod (η (a, a).2)) = κ a
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 γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
b : β
hb : b ∈ s
⊢ (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
b : β
hb : b ∉ s
⊢ (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
b : β
hb : b ∈ s
⊢ (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
b : β
hb : b ∉ s
⊢ (η (x, b)) {_c | b ∈ s} = s.indicator (fun x ↦ 1) b
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 α β
f : β → γ
hf : Measurable f
⊢ map f (⇑κ ∘ₘ μ) = ⇑(κ.map f) ∘ₘ μ

Tactic:
ext s hs
  rw [Measure.map_apply hf hs, Measure.bind_apply (hf hs) κ.aemeasurable,
    Measure.bind_apply hs (Kernel.aemeasurable _)]
  simp_rw [Kernel.map_apply' _ hf _ hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x) (κ x)}

Tactic:
exact measurableSet_lt (Measurable.lintegral_kernel_prod_right hf.enorm) measurable_const

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

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ ⇑κ ∘ₘ (boolKernel μ ν) false = (boolKernel (⇑κ ∘ₘ μ) (⇑κ ∘ₘ ν)) false

pp: case true
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ ⇑κ ∘ₘ (boolKernel μ ν) true = (boolKernel (⇑κ ∘ₘ μ) (⇑κ ∘ₘ ν)) true

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ ⇑κ ∘ₘ (boolKernel μ ν) false = (boolKernel (⇑κ ∘ₘ μ) (⇑κ ∘ₘ ν)) false

case true
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ ⇑κ ∘ₘ (boolKernel μ ν) true = (boolKernel (⇑κ ∘ₘ μ) (⇑κ ∘ₘ ν)) true