awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
h :
  ∀ (ω : Ω) (hω₁ : μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t)
    (hω₂ :
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
        μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s,
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)

Tactic:
filter_upwards [condExp_set_generateFrom_singleton hs ht, this] with ω hω₁ hω₂

Premises used: ProbabilityTheory.condExp_set_generateFrom_singleton
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω
h :
  ∀
    (hω₂ :
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
        μ[|s].real t),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
h₁ :
  ∀
    (hω₂ :
      ENNReal.toReal
          ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
              (a : Set Ω) → ℝ≥0∞)
            t) =
        μ[|s].real t),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
h₂ :
  ∀
    (hω₂ :
      ENNReal.toReal
          ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
              (a : Set Ω) → ℝ≥0∞)
            t) =
        ENNReal.toReal μ[t | s]),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
h₃ h₄ h₅ h₆ :
  ∀
    (hω₂ :
      Eq (α := ℝ≥0∞)
        ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
              (a : Set Ω) → ℝ≥0∞)
            t :
          ℝ≥0∞)
        (μ[t | s] : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)

Tactic:
rwa [hω₁, measureReal_def, measureReal_def,
    ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂

Premises used: ENNReal.toReal_eq_toReal_iff', MeasureTheory.measure_ne_top, MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
f g : Kernel α β
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → Measure β) (measurable' : Measurable toFun)
    (h : { toFun := toFun, measurable' := measurable' : Kernel α β }.toFun = g.toFun),
    { toFun := toFun, measurable' := measurable' : Kernel α β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
g : Kernel α β
toFun : α → Measure β
measurable' : Measurable toFun
h : { toFun := toFun, measurable' := measurable' : Kernel α β }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → Measure β) (measurable'_1 : Measurable toFun_1)
    (h :
      { toFun := toFun, measurable' := measurable' : Kernel α β }.toFun =
        { toFun := toFun_1, measurable' := measurable'_1 : Kernel α β }.toFun),
    { toFun := toFun, measurable' := measurable' : Kernel α β } = { toFun := toFun_1, measurable' := measurable'_1 }
⊢ { toFun := toFun, measurable' := measurable' : Kernel α β } = g

Tactic:
cases g
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
toFun : α → Measure β
measurable' : Measurable toFun
toFun_1 : α → Measure β
measurable'_1 : Measurable toFun_1
h :
  { toFun := toFun, measurable' := measurable' : Kernel α β }.toFun =
    { toFun := toFun_1, measurable' := measurable'_1 : Kernel α β }.toFun
⊢ { toFun := toFun, measurable' := measurable' : Kernel α β } = { toFun := toFun_1, measurable' := measurable'_1 }

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ Measurable.{u_1, u_2} (α := α) (β := Measure β) (⇑κ : (a : α) → Measure β)

Tactic:
κ.measurable'

Premises used: ProbabilityTheory.Kernel.measurable'
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
⊢ AEMeasurable.{u_1, u_2} (β := Measure β) (⇑κ : (a : α) → Measure β) μ

Tactic:
κ.measurable.aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
⊢ (⇑{ toFun := f, measurable' := hf : Kernel α β } : (a : α) → Measure β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Eq (α := (a : α) → Measure β) (⇑0 : (a : α) → Measure β) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ (⇑(κ + η) : (a : α) → Measure β) =
    HAdd.hAdd (α := (a : α) → Measure β) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
n : ℕ
κ : Kernel α β
⊢ (⇑(n • κ) : (a : α) → Measure β) = HSMul.hSMul (β := (a : α) → Measure β) n (⇑κ : (a : α) → Measure β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) (((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) (0 : Measure β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
⊢ (κ + η : (a : α) → Measure β) a =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η : (a : α) → Measure β) a : Measure β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
n : ℕ
κ : Kernel α β
a : α
⊢ (n • κ : (a : α) → Measure β) a = HSMul.hSMul (β := Measure β) n ((κ : (a : α) → Measure β) a : Measure β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
x : Kernel α β
n : ℕ
⊢ (⇑(n • x) : (a : α) → Measure β) = HSMul.hSMul (β := (a : α) → Measure β) n (⇑x : (a : α) → Measure β)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α_1 : Type u_1
β_1 : Type u_2
ι : Type u_3
mα : MeasurableSpace α_1
mβ : MeasurableSpace β_1
α : Type u_4
β : Type u_5
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ AddLeftMono (Kernel α β)

Tactic:
⟨fun _ _ _ hμ a ↦ add_le_add_right (hμ a) _⟩

Premises used: CovariantClass.mk, add_le_add_right, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α_1 : Type u_1
β_1 : Type u_2
ι : Type u_3
mα : MeasurableSpace α_1
mβ : MeasurableSpace β_1
α : Type u_4
β : Type u_5
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
κ : Kernel α β
a : α
⊢ LE.le.{u_5} (α := (fun (a : α) ↦ Measure β) a)
    ((fun (f : Kernel α β) ↦ ((⇑f : (a : α) → Measure β) : (a : α) → Measure β)) 0 a)
    ((fun (f : Kernel α β) ↦ ((⇑f : (a : α) → Measure β) : (a : α) → Measure β)) κ a)

Tactic:
simp only [coe_zero, Pi.zero_apply, Measure.zero_le]

Premises used: ProbabilityTheory.Kernel.coe_zero, Pi.zero_apply, MeasureTheory.Measure.zero_le
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_4
β : Type u_5
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
κ : Kernel α β
⊢ Eq (α := α → Measure β) ((coeAddHom α β : (a : Kernel α β) → α → Measure β) κ : α → Measure β)
    ((⇑κ : (a : α) → Measure β) : (a : α) → Measure β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
⊢ Eq (α := (a : α) → Measure β) (⇑(∑ i ∈ I, κ i) : (a : α) → Measure β) (∑ i ∈ I, (⇑(κ i) : (a : α) → Measure β))

Tactic:
map_sum (coeAddHom α β) _ _

Premises used: ProbabilityTheory.Kernel.coeAddHom, map_sum
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
rw :
  Eq.{u_2 + 1} (α := Measure β) ((∑ i ∈ I, (⇑(κ i) : (a : α) → Measure β)) a) (∑ i ∈ I, (κ i : (a : α) → Measure β) a)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Measure β) (∑ c ∈ I, (κ c : (a : α) → Measure β) a) (∑ i ∈ I, (κ i : (a : α) → Measure β) a)
⊢ Eq.{u_2 + 1} (α := Measure β) (((∑ i ∈ I, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β)
    (∑ i ∈ I, (κ i : (a : α) → Measure β) a : Measure β)

Tactic:
rw [coe_finsetSum, Finset.sum_apply]

Premises used: Finset.sum_apply, ProbabilityTheory.Kernel.coe_finsetSum
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((∑ i ∈ I, (κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (((((∑ i ∈ I, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [finsetSum_apply, Measure.finsetSum_apply]

Premises used: MeasureTheory.Measure.finsetSum_apply, ProbabilityTheory.Kernel.finsetSum_apply
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsZeroOrMarkovKernel κ
⊢ κ = 0 ∨ IsMarkovKernel κ

Tactic:
h.eq_zero_or_isMarkovKernel'

Premises used: ProbabilityTheory.IsZeroOrMarkovKernel.eq_zero_or_isMarkovKernel'
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
obtain :
  ∀ (C : ℝ≥0∞) (hC : C < ∞)
    (hle : ∀ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ C), κ.bound < ∞
⊢ κ.bound < ∞

Tactic:
obtain ⟨C, hC, hle⟩ := h.exists_univ_le

Premises used: ProbabilityTheory.IsFiniteKernel.exists_univ_le
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
C : ℝ≥0∞
hC : C < ∞
hle : ∀ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ C
⊢ κ.bound < ∞

Tactic:
lt_of_le_of_lt ?_ hC

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
C : ℝ≥0∞
hC : C < ∞
hle : ∀ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ C
refine : κ.bound ≤ C
⊢ κ.bound < ∞

Tactic:
refine lt_of_le_of_lt ?_ hC

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
C : ℝ≥0∞
hC : C < ∞
hle : ∀ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ C
⊢ κ.bound ≤ C

Tactic:
simp [bound, hle]

Premises used: ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
⊢ κ.bound ≠ ∞

Tactic:
κ.bound_lt_top.ne

Premises used: ProbabilityTheory.Kernel.bound_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s : Set β
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ≤ κ.bound

Tactic:
(measure_mono (Set.subset_univ s)).trans <| le_iSup (f := fun a ↦ κ a .univ) a

Premises used: Set.subset_univ, Set.univ, le_iSup, MeasureTheory.measure_mono, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : IsEmpty α
κ : Kernel α β
⊢ κ.bound = 0

Tactic:
simp [bound]

Premises used: ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : IsEmpty β
κ : Kernel α β
⊢ κ.bound = 0

Tactic:
simp [bound, Subsingleton.elim _ (0 : Measure β)]

Premises used: Subsingleton.elim, OfNat.ofNat, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ bound.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0 = 0

Tactic:
simp [bound]

Premises used: ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α_1 : Type u_1
β_1 : Type u_2
ι : Type u_3
mα : MeasurableSpace α_1
mβ : MeasurableSpace β_1
α : Type u_4
β : Type u_5
x : MeasurableSpace α
x_1 : MeasurableSpace β
x_2 : α
⊢ LE.le (α := ℝ≥0∞) (((((0 : Kernel α β) : (a : α) → Measure β) x_2 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ IsFiniteKernel (κ + η)

Tactic:
⟨⟨κ.bound + η.bound, ENNReal.add_lt_top.mpr ⟨κ.bound_lt_top, η.bound_lt_top⟩, fun a => ?_⟩⟩

Premises used: Iff.mpr, ProbabilityTheory.IsFiniteKernel.mk, ProbabilityTheory.Kernel.bound_lt_top, HAdd.hAdd, And.intro, Exists.intro, ENNReal.add_lt_top, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
refine : ∀ (a : α), (((κ + η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound + η.bound
⊢ IsFiniteKernel (κ + η)

Tactic:
refine ⟨⟨κ.bound + η.bound, ENNReal.add_lt_top.mpr ⟨κ.bound_lt_top, η.bound_lt_top⟩, fun a => ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ (((κ + η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound + η.bound

Tactic:
add_le_add (Kernel.measure_le_bound _ _ _) (Kernel.measure_le_bound _ _ _)

Premises used: add_le_add, WithTop.map₂, ProbabilityTheory.Kernel.measure_le_bound, Option.map₂
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ (((κ + η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound + η.bound

Tactic:
exact add_le_add (Kernel.measure_le_bound _ _ _) (Kernel.measure_le_bound _ _ _)

Premises used: add_le_add, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ ν : Kernel α β
hν : IsFiniteKernel ν
hκν : κ ≤ ν
⊢ IsFiniteKernel κ

Tactic:
⟨ν.bound, ν.bound_lt_top, fun a ↦ (hκν _ _).trans (ν.measure_le_bound a Set.univ)⟩

Premises used: Set.univ, ProbabilityTheory.IsFiniteKernel.mk, ProbabilityTheory.Kernel.bound_lt_top, And.intro, ProbabilityTheory.Kernel.measure_le_bound, Exists.intro, LE.le.trans, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsMarkovKernel κ
a : α
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
IsMarkovKernel.isProbabilityMeasure a

Premises used: ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
⟨Or.inl rfl⟩

Premises used: ProbabilityTheory.IsZeroOrMarkovKernel.mk, Or.inl, rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsMarkovKernel κ
⊢ ProbabilityTheory.IsZeroOrMarkovKernel κ

Tactic:
⟨Or.inr h⟩

Premises used: ProbabilityTheory.IsZeroOrMarkovKernel.mk, Or.inr
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsZeroOrMarkovKernel κ
a : α
inl :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) (((0 : Kernel α β) : (a : α) → Measure β) a)
inr : ∀ (h' : IsMarkovKernel κ), IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h'

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
η : Kernel α β
a : α
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsZeroOrMarkovKernel κ
a : α
h' : IsMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
a : α
⊢ IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
⟨(κ.measure_le_bound a Set.univ).trans_lt κ.bound_lt_top⟩

Premises used: Set.univ, ProbabilityTheory.Kernel.bound_lt_top, ProbabilityTheory.Kernel.measure_le_bound, MeasureTheory.IsFiniteMeasure.mk, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsZeroOrMarkovKernel κ
inl :
  ∀ [h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
inr : ∀ (_h' : IsMarkovKernel κ), IsFiniteKernel κ
⊢ IsFiniteKernel κ

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | _h'

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
η : Kernel α β
h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsZeroOrMarkovKernel κ
_h' : IsMarkovKernel κ
⊢ IsFiniteKernel κ

Tactic:
⟨⟨1, ENNReal.one_lt_top, fun _ => prob_le_one⟩⟩

Premises used: ProbabilityTheory.IsFiniteKernel.mk, MeasureTheory.prob_le_one, ENNReal.one_lt_top, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsZeroOrMarkovKernel κ
_h' : IsMarkovKernel κ
⊢ IsFiniteKernel κ

Tactic:
exact ⟨⟨1, ENNReal.one_lt_top, fun _ => prob_le_one⟩⟩
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Nonempty α
κ : Kernel α β
inst_1 : IsMarkovKernel κ
⊢ κ.bound = 1

Tactic:
simp [bound]

Premises used: ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
inl : IsEmpty α → κ.bound ≤ 1
inr : Nonempty α → κ.bound ≤ 1
⊢ κ.bound ≤ 1

Tactic:
rcases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
h : IsEmpty α
⊢ κ.bound ≤ 1

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
h : Nonempty α
inr :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    bound.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0 ≤ 1
inr₁ : IsMarkovKernel κ → κ.bound ≤ 1
⊢ κ.bound ≤ 1

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | _

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
h : Nonempty α
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ bound.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0 ≤ 1

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
h : Nonempty α
h_1 : IsMarkovKernel κ
⊢ κ.bound ≤ 1

Tactic:
simp