awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
⊢ ∀ (i : 𝓨),
    ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), avgRisk ℓ P κ π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ i)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
fun y ↦ iInf_le_of_le (Kernel.const _ (Measure.dirac y)) ?_

Premises used: MeasureTheory.Measure.dirac, iInf_le_of_le, ProbabilityTheory.Kernel.const
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
refine :
  ∀ (y : 𝓨),
    ⨅ (_ : IsMarkovKernel (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac y))),
        avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac y)) π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
⊢ ∀ (i : 𝓨),
    ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), avgRisk ℓ P κ π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ i)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
refine fun y ↦ iInf_le_of_le (Kernel.const _ (Measure.dirac y)) ?_

Premises used: MeasureTheory.Measure.dirac, iInf_le_of_le, ProbabilityTheory.Kernel.const
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
simp :
  ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
⊢ ⨅ (_ : IsMarkovKernel (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac y))),
      avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac y)) π ≤
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
simp only [iInf_pos, avgRisk_const_right', mul_comm]

Premises used: mul_comm, ProbabilityTheory.avgRisk_const_right', iInf_pos
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
hfg : ∀ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y ≤ ℓ θ y
⊢ ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
gcongr with θ
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
θ : Θ
⊢ Measurable (ℓ θ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
θ : Θ
hfg hfg₁ : ℓ θ y ≤ ℓ θ y
⊢ ∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y ≤ ℓ θ y

Tactic:
rw [lintegral_dirac' _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_dirac'
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
π : Measure Θ
⊢ Eq (α := ℝ≥0∞)
    (⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)
    (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π)

Tactic:
simp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
⊢ Eq (α := ℝ≥0∞)
    (⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          (((((Kernel.const Θ μ : Kernel Θ 𝓧) : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ :
            ℝ≥0∞) ∂π)
    (⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)

Tactic:
simp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
refine :
  ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    bayesRisk ℓ (Kernel.const Θ μ) π
⊢ bayesRisk ℓ (Kernel.const Θ μ) π =
    ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
refine le_antisymm ((bayesRisk_le_iInf' hl _ _).trans_eq (by simp)) ?_

Premises used: LE.le.trans_eq, le_antisymm, ProbabilityTheory.bayesRisk_le_iInf'
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
simp_rw :
  ∀ (i : Kernel 𝓧 𝓨) (i_1 : IsMarkovKernel i),
    ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
      avgRisk ℓ (Kernel.const Θ μ) i π
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    bayesRisk ℓ (Kernel.const Θ μ) π

Tactic:
simp_rw [bayesRisk, le_iInf_iff]

Premises used: ProbabilityTheory.bayesRisk, le_iInf_iff
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
rw :
  ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    avgRisk ℓ (Kernel.const Θ μ) κ π

Tactic:
rw [avgRisk_const_left' hl]

Premises used: ProbabilityTheory.avgRisk_const_left'
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ

Tactic:
le_trans ?_ (iInf_mul_le_lintegral (fun y ↦ ∫⁻ θ, ℓ θ y ∂π))

Premises used: MeasureTheory.iInf_mul_le_lintegral, MeasureTheory.lintegral, le_trans
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
refine :
  ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : 𝓨), ∫⁻ (θ : Θ), ℓ θ x ∂π : ℝ≥0∞)
      ((((⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ

Tactic:
refine le_trans ?_ (iInf_mul_le_lintegral (fun y ↦ ∫⁻ θ, ℓ θ y ∂π))

Premises used: MeasureTheory.iInf_mul_le_lintegral, MeasureTheory.lintegral, le_trans
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0

Tactic:
simpa using hμ
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
rw :
  LE.le (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)
    (⨅ (i : 𝓨), HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ i ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : 𝓨), ∫⁻ (θ : Θ), ℓ θ x ∂π : ℝ≥0∞)
      ((((⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rw [Measure.comp_apply_univ, ENNReal.iInf_mul' hl_pos (fun hμ ↦ h_zero (by simpa using hμ))]

Premises used: MeasureTheory.Measure.comp_apply_univ, ENNReal.iInf_mul'
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
h :
  ∀ (y : 𝓨),
    ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
      HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ y ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)
    (⨅ (i : 𝓨), HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ i ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))

Tactic:
gcongr with y
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
y : 𝓨
h : Measurable (β := ℝ≥0∞) fun (θ : Θ) ↦ ℓ θ y
⊢ ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ y ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rw [lintegral_mul_const]

Premises used: MeasureTheory.lintegral_mul_const
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
y : 𝓨
⊢ Measurable (β := ℝ≥0∞) fun (θ : Θ) ↦ ℓ θ y

Tactic:
fun_prop
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : NeZero μ
inst_1 : IsFiniteMeasure μ
π : Measure Θ
inst_2 : SFinite π
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0

Tactic:
simp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : NeZero μ
inst_1 : IsFiniteMeasure μ
π : Measure Θ
inst_2 : SFinite π
⊢ μ = 0 → Nonempty 𝓨

Tactic:
simp [NeZero.out]

Premises used: NeZero.out
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst : Nonempty 𝓨
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst_1 : IsFiniteMeasure μ
π : Measure Θ
inst_2 : SFinite π
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0

Tactic:
simp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : IsProbabilityMeasure μ
π : Measure Θ
inst_1 : SFinite π
⊢ bayesRisk ℓ (Kernel.const Θ μ) π = ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π

Tactic:
simp [bayesRisk_const_of_neZero hl μ π]

Premises used: ProbabilityTheory.bayesRisk_const_of_neZero
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC hfg : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
    ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), (↑C : ℝ≥0∞) ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π

Tactic:
gcongr with θ y
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
θ : Θ
y : 𝓨
⊢ ℓ θ y ≤ (↑C : ℝ≥0∞)

Tactic:
hℓC θ y
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
θ : Θ
y : 𝓨
⊢ ℓ θ y ≤ (↑C : ℝ≥0∞)

Tactic:
exact hℓC θ y
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), (↑C : ℝ≥0∞) ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π =
    ∫⁻ (θ : Θ),
      (↑C : ℝ≥0∞) *
        ∫⁻ (x : 𝓧),
          (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ ∂(P : (a : Θ) → Measure 𝓧) θ ∂π

Tactic:
simp [Kernel.comp_apply' _ _ _ .univ]

Premises used: ProbabilityTheory.Kernel.comp_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
hfg : ∀ (θ : Θ) (x : 𝓧), (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ ∫⁻ (θ : Θ),
      (↑C : ℝ≥0∞) *
        ∫⁻ (x : 𝓧),
          (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ ∂(P : (a : Θ) → Measure 𝓧) θ ∂π ≤
    ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * ∫⁻ (x : 𝓧), κ.bound ∂(P : (a : Θ) → Measure 𝓧) θ ∂π

Tactic:
gcongr with θ x
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
θ : Θ
x : 𝓧
⊢ (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
Kernel.measure_le_bound κ x Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
θ : Θ
x : 𝓧
⊢ (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
exact Kernel.measure_le_bound κ x Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
simp :
  ∫⁻ (θ : Θ),
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound)
      ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
| ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * ∫⁻ (x : 𝓧), κ.bound ∂(P : (a : Θ) → Measure 𝓧) θ ∂π

Tactic:
simp only [lintegral_const, ← mul_assoc]

Premises used: MeasureTheory.lintegral_const, mul_assoc
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
conv_lhs :
  ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * κ.bound * P.bound ∂π
⊢ ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * ∫⁻ (x : 𝓧), κ.bound ∂(P : (a : Θ) → Measure 𝓧) θ ∂π ≤
    ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * κ.bound * P.bound ∂π

Tactic:
conv_lhs => simp only [lintegral_const, ← mul_assoc]

Premises used: MeasureTheory.lintegral_const, mul_assoc
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
hfg : ∀ (θ : Θ), (((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ ≤ P.bound
⊢ ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * κ.bound * P.bound ∂π

Tactic:
gcongr with θ
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
θ : Θ
⊢ (((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ ≤ P.bound

Tactic:
Kernel.measure_le_bound P θ Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
θ : Θ
⊢ (((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ ≤ P.bound

Tactic:
exact Kernel.measure_le_bound P θ Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * κ.bound * P.bound ∂π =
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ avgRisk ℓ P κ π ≤ (↑C : ℝ≥0∞)

Tactic:
(avgRisk_le_mul' P κ π hℓC).trans ?_

Premises used: ProbabilityTheory.avgRisk_le_mul', LE.le.trans
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
refine :
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ avgRisk ℓ P κ π ≤ (↑C : ℝ≥0∞)

Tactic:
refine (avgRisk_le_mul' P κ π hℓC).trans ?_

Premises used: ProbabilityTheory.avgRisk_le_mul', LE.le.trans