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∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
inl :
  IsEmpty Θ →
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
inr :
  Nonempty Θ →
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)

Tactic:
rcases isEmpty_or_nonempty Θ

Premises used: isEmpty_or_nonempty
-- 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∞)
h : IsEmpty Θ
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥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∞)
h : Nonempty Θ
inr :
  IsEmpty 𝓧 →
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
inr₁ :
  Nonempty 𝓧 →
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)

Tactic:
rcases isEmpty_or_nonempty 𝓧

Premises used: isEmpty_or_nonempty
-- 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∞)
h : Nonempty Θ
h_1 : IsEmpty 𝓧
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥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∞)
h : Nonempty Θ
h_1 : Nonempty 𝓧
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥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∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ bayesRisk ℓ P π ≤ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
(bayesRisk_le_avgRisk ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π).trans ?_

Premises used: Nonempty.some, MeasureTheory.Measure.dirac, ProbabilityTheory.bayesRisk_le_avgRisk, LE.le.trans, 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∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
refine :
  avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ bayesRisk ℓ P π ≤ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
refine (bayesRisk_le_avgRisk ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π).trans ?_

Premises used: Nonempty.some, MeasureTheory.Measure.dirac, ProbabilityTheory.bayesRisk_le_avgRisk, LE.le.trans, 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∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
(avgRisk_le_mul' P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π hℓC).trans ?_

Premises used: ProbabilityTheory.avgRisk_le_mul', Nonempty.some, MeasureTheory.Measure.dirac, LE.le.trans, 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∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
refine :
  HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
refine (avgRisk_le_mul' P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π hℓC).trans ?_

Premises used: ProbabilityTheory.avgRisk_le_mul', Nonempty.some, MeasureTheory.Measure.dirac, LE.le.trans, 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∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
inl :
  IsEmpty 𝓧 →
    HMul.hMul (β := ℝ≥0∞)
        ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
        ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
inr :
  Nonempty 𝓧 →
    HMul.hMul (β := ℝ≥0∞)
        ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
        ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rcases isEmpty_or_nonempty 𝓧

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
h : IsEmpty 𝓧
⊢ HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * 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∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
h : Nonempty 𝓧
⊢ HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * 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∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ bayesRisk ℓ P π ≤ (↑C : ℝ≥0∞)

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

Premises used: ProbabilityTheory.bayesRisk_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∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
refine : HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ bayesRisk ℓ P π ≤ (↑C : ℝ≥0∞)

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

Premises used: ProbabilityTheory.bayesRisk_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∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
inl : IsEmpty Θ → HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
inr :
  Nonempty Θ → HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)

Tactic:
rcases isEmpty_or_nonempty Θ

Premises used: isEmpty_or_nonempty
-- 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 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
h : IsEmpty Θ
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥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∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
h : Nonempty Θ
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥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∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsFiniteKernel P
π : Measure Θ
inst_2 : IsFiniteMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ bayesRisk ℓ P π < ∞

Tactic:
(bayesRisk_le_mul' P π hℓC).trans_lt ?_

Premises used: ProbabilityTheory.bayesRisk_le_mul', LE.le.trans_lt
-- 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 𝓨
P : Kernel Θ 𝓧
inst_1 : IsFiniteKernel P
π : Measure Θ
inst_2 : IsFiniteMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
refine : HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) < ∞
⊢ bayesRisk ℓ P π < ∞

Tactic:
refine (bayesRisk_le_mul' P π hℓC).trans_lt ?_

Premises used: ProbabilityTheory.bayesRisk_le_mul', LE.le.trans_lt
-- 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 𝓨
P : Kernel Θ 𝓧
inst_1 : IsFiniteKernel P
π : Measure Θ
inst_2 : IsFiniteMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) < ∞

Tactic:
simp [ENNReal.mul_lt_top_iff, P.bound_lt_top]

Premises used: ENNReal.mul_lt_top_iff, ProbabilityTheory.Kernel.bound_lt_top
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
π : Measure Θ
inst : SFinite π
rw :
  bayesRisk (m𝓧 := PUnit.instMeasurableSpace) ℓ (Kernel.const Θ (Measure.dirac PUnit.unit)) π =
    ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π
rw₁ rw₂ : Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π)
⊢ bayesRisk ℓ (Kernel.discard Θ) π = ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π

Tactic:
rw [Kernel.discard_eq_const, bayesRisk_const hl]

Premises used: ProbabilityTheory.bayesRisk_const, ProbabilityTheory.Kernel.discard_eq_const
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
inl :
  ∀ (hX : IsEmpty 𝓧),
    bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
inr :
  ∀ (hX : Nonempty 𝓧),
    bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

Tactic:
rcases isEmpty_or_nonempty 𝓧 with hX | hX

Premises used: isEmpty_or_nonempty
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : IsEmpty 𝓧
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

Tactic:
simp [iInf_subtype']

Premises used: iInf_subtype'
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : Nonempty 𝓧
inr : ∀ (x : 𝓧), bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

Tactic:
obtain x := hX.some

Premises used: Nonempty.some
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
inr :
  Eq (α := ℝ≥0∞) (⨅ (x : Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel), avgRisk ℓ P (↑x : Kernel 𝓧 𝓨) π)
    (⨅ (x : Subtype (α := Measure 𝓨) IsProbabilityMeasure), avgRisk ℓ P (Kernel.const 𝓧 (↑x : Measure 𝓨)) π)
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

Tactic:
rw [bayesRisk, iInf_subtype', iInf_subtype']

Premises used: ProbabilityTheory.bayesRisk, iInf_subtype'
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }
a :
  ∀ (y : 𝓧) (s : Set 𝓨),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((((↑((fun (μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) ↦
                              (Subtype.mk (p := fun (κ : Kernel 𝓧 𝓨) ↦ IsMarkovKernel κ)
                                  (Kernel.const 𝓧 (↑μ : Measure 𝓨)) ⋯ :
                                { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }))
                            ((fun (κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) ↦
                                (Subtype.mk (p := fun (μ : Measure 𝓨) ↦ IsProbabilityMeasure μ)
                                    (((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) x) ⋯ :
                                  { μ : Measure 𝓨 // IsProbabilityMeasure μ }))
                              κ)) :
                        Kernel 𝓧 𝓨) :
                      Kernel 𝓧 𝓨) :
                    (a : 𝓧) → Measure 𝓨)
                  y :
                Measure 𝓨) :
              (a : Set 𝓨) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        (((((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) y : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (fun (μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) ↦
        (Subtype.mk (p := fun (κ : Kernel 𝓧 𝓨) ↦ IsMarkovKernel κ) (Kernel.const 𝓧 (↑μ : Measure 𝓨)) ⋯ :
          { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }))
      ((fun (κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) ↦
          (Subtype.mk (p := fun (μ : Measure 𝓨) ↦ IsProbabilityMeasure μ) (((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) x)
              ⋯ :
            { μ : Measure 𝓨 // IsProbabilityMeasure μ }))
        κ) =
    κ

Tactic:
ext 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }
y : 𝓧
s : Set 𝓨
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((((↑((fun (μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) ↦
                          (Subtype.mk (p := fun (κ : Kernel 𝓧 𝓨) ↦ IsMarkovKernel κ) (Kernel.const 𝓧 (↑μ : Measure 𝓨))
                              ⋯ :
                            { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }))
                        ((fun (κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) ↦
                            (Subtype.mk (p := fun (μ : Measure 𝓨) ↦ IsProbabilityMeasure μ)
                                (((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) x) ⋯ :
                              { μ : Measure 𝓨 // IsProbabilityMeasure μ }))
                          κ)) :
                    Kernel 𝓧 𝓨) :
                  Kernel 𝓧 𝓨) :
                (a : 𝓧) → Measure 𝓨)
              y :
            Measure 𝓨) :
          (a : Set 𝓨) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) y : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [Kernel.const_apply, Subsingleton.elim x y]

Premises used: ProbabilityTheory.Kernel.const_apply, Subsingleton.elim
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }
⊢ (fun (κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) ↦
        (Subtype.mk (p := fun (μ : Measure 𝓨) ↦ IsProbabilityMeasure μ) (((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) x)
            ⋯ :
          { μ : Measure 𝓨 // IsProbabilityMeasure μ }))
      ((fun (μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) ↦
          (Subtype.mk (p := fun (κ : Kernel 𝓧 𝓨) ↦ IsMarkovKernel κ) (Kernel.const 𝓧 (↑μ : Measure 𝓨)) ⋯ :
            { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }))
        μ) =
    μ

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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
e : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ } ≃ { μ : Measure 𝓨 // IsProbabilityMeasure μ } :=
  {
    toFun := fun (κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) ↦
      Subtype.mk (p := fun (μ : Measure 𝓨) ↦ IsProbabilityMeasure μ) (((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) x) ⋯,
    invFun := fun (μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) ↦
      Subtype.mk (p := fun (κ : Kernel 𝓧 𝓨) ↦ IsMarkovKernel κ) (Kernel.const 𝓧 (↑μ : Measure 𝓨)) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
inr :
  Eq (α := ℝ≥0∞)
    (⨅ (x : { μ : Measure 𝓨 // IsProbabilityMeasure μ }),
      avgRisk (m𝓨 := m𝓨) ℓ P
        (↑((e.symm : (a : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) → { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) x) :
          Kernel 𝓧 𝓨)
        π)
    (⨅ (x : Subtype (α := Measure 𝓨) IsProbabilityMeasure), avgRisk ℓ P (Kernel.const 𝓧 (↑x : Measure 𝓨)) π)
⊢ Eq (α := ℝ≥0∞) (⨅ (x : Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel), avgRisk ℓ P (↑x : Kernel 𝓧 𝓨) π)
    (⨅ (x : Subtype (α := Measure 𝓨) IsProbabilityMeasure), avgRisk ℓ P (Kernel.const 𝓧 (↑x : Measure 𝓨)) π)

Tactic:
rw [← Equiv.iInf_comp e.symm]

Premises used: Equiv.iInf_comp, Equiv.symm
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
hX : Nonempty 𝓧
x : 𝓧
e : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ } ≃ { μ : Measure 𝓨 // IsProbabilityMeasure μ } :=
  {
    toFun := fun (κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) ↦
      Subtype.mk (p := fun (μ : Measure 𝓨) ↦ IsProbabilityMeasure μ) (((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) x) ⋯,
    invFun := fun (μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) ↦
      Subtype.mk (p := fun (κ : Kernel 𝓧 𝓨) ↦ IsMarkovKernel κ) (Kernel.const 𝓧 (↑μ : Measure 𝓨)) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Eq (α := ℝ≥0∞)
    (⨅ (x : { μ : Measure 𝓨 // IsProbabilityMeasure μ }),
      avgRisk (m𝓨 := m𝓨) ℓ P
        (↑((e.symm : (a : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) → { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) x) :
          Kernel 𝓧 𝓨)
        π)
    (⨅ (x : Subtype (α := Measure 𝓨) IsProbabilityMeasure), avgRisk ℓ P (Kernel.const 𝓧 (↑x : Measure 𝓨)) π)

Tactic:
rfl
-- 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
inst_2 : SFinite π
hl : Measurable (uncurry ℓ)
⊢ bayesRisk ℓ P π =
    ⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
le_antisymm (bayesRisk_le_iInf' hl _ _) ?_

Premises used: 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∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
inst_2 : SFinite π
hl : Measurable (uncurry ℓ)
refine :
  ⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    bayesRisk ℓ P π
⊢ bayesRisk ℓ P π =
    ⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π

Tactic:
refine le_antisymm (bayesRisk_le_iInf' hl _ _) ?_

Premises used: le_antisymm, ProbabilityTheory.bayesRisk_le_iInf'