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

Tactic:
rw [bayesRisk_eq_iInf_measure_of_subsingleton]

Premises used: ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton
-- 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 ℓ)
simp :
  ∀ (i : Measure 𝓨) (i_1 : IsProbabilityMeasure i),
    ⨅ (y : 𝓨),
        ∫⁻ (θ : Θ),
          HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
            ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
          (∫⁻ (y : 𝓨), ℓ θ y ∂i) ∂π
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)
    (⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π)

Tactic:
simp only [avgRisk_const_right', le_iInf_iff]

Premises used: le_iInf_iff, ProbabilityTheory.avgRisk_const_right'
-- 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 ℓ)
⊢ ∀ (i : Measure 𝓨) (i_1 : IsProbabilityMeasure i),
    ⨅ (y : 𝓨),
        ∫⁻ (θ : Θ),
          HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
            ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
          (∫⁻ (y : 𝓨), ℓ θ y ∂i) ∂π

Tactic:
fun μ hμ ↦ (iInf_le_lintegral (μ := μ) _).trans_eq ?_

Premises used: HMul.hMul, LE.le.trans_eq, Set.univ, MeasureTheory.iInf_le_lintegral, DFunLike.coe, MeasureTheory.lintegral
-- 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 :
  ∀ (μ : Measure 𝓨) (hμ : IsProbabilityMeasure μ),
    ∫⁻ (x : 𝓨),
        ∫⁻ (θ : Θ),
          HMul.hMul (β := ℝ≥0∞) (ℓ θ x)
            ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ∂μ =
      ∫⁻ (θ : Θ),
        HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
          (∫⁻ (y : 𝓨), ℓ θ y ∂μ) ∂π
⊢ ∀ (i : Measure 𝓨) (i_1 : IsProbabilityMeasure i),
    ⨅ (y : 𝓨),
        ∫⁻ (θ : Θ),
          HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
            ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
          (∫⁻ (y : 𝓨), ℓ θ y ∂i) ∂π

Tactic:
refine fun μ hμ ↦ (iInf_le_lintegral (μ := μ) _).trans_eq ?_
-- 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 ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
rw :
  ∫⁻ (y : Θ),
      ∫⁻ (x : 𝓨),
        HMul.hMul (β := ℝ≥0∞) (ℓ y x)
          ((((P : (a : Θ) → Measure 𝓧) y : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂μ ∂π =
    ∫⁻ (θ : Θ),
      HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (∫⁻ (y : 𝓨), ℓ θ y ∂μ) ∂π
hf :
  AEMeasurable (β := ℝ≥0∞)
    (uncurry fun (x : 𝓨) (θ : Θ) ↦
      HMul.hMul (β := ℝ≥0∞) (ℓ θ x) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))
    (μ.prod π)
⊢ ∫⁻ (x : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ x)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ∂μ =
    ∫⁻ (θ : Θ),
      HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (∫⁻ (y : 𝓨), ℓ θ y ∂μ) ∂π

Tactic:
rw [lintegral_lintegral_swap]

Premises used: MeasureTheory.lintegral_lintegral_swap
-- 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 ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
e_f :
  ∀ (θ : Θ),
    ∫⁻ (x : 𝓨),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ x)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂μ =
      HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (∫⁻ (y : 𝓨), ℓ θ y ∂μ)
⊢ ∫⁻ (y : Θ),
      ∫⁻ (x : 𝓨),
        HMul.hMul (β := ℝ≥0∞) (ℓ y x)
          ((((P : (a : Θ) → Measure 𝓧) y : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂μ ∂π =
    ∫⁻ (θ : Θ),
      HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (∫⁻ (y : 𝓨), ℓ θ y ∂μ) ∂π

Tactic:
congr 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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
inst_2 : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
θ : Θ
⊢ 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∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
inst_2 : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
θ : Θ
e_f :
  HMul.hMul (β := ℝ≥0∞) (∫⁻ (a : 𝓨), ℓ θ a ∂μ)
      ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (∫⁻ (y : 𝓨), ℓ θ y ∂μ)
e_f₁ e_f₂ :
  HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (∫⁻ (a : 𝓨), ℓ θ a ∂μ) =
    HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (∫⁻ (y : 𝓨), ℓ θ y ∂μ)
⊢ ∫⁻ (x : 𝓨),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ x)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂μ =
    HMul.hMul (α := ℝ≥0∞) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (∫⁻ (y : 𝓨), ℓ θ y ∂μ)

Tactic:
rw [lintegral_mul_const _ (by fun_prop), mul_comm]

Premises used: MeasureTheory.lintegral_mul_const, mul_comm
-- 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 ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ Measurable (β := ℝ≥0∞) fun (a : Θ) ↦ (((P : (a : Θ) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ

Tactic:
have := P.measurable_coe .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 Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
inst_2 : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
this : Measurable (β := ℝ≥0∞) fun (a : Θ) ↦ (((P : (a : Θ) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ
⊢ AEMeasurable (β := ℝ≥0∞)
    (uncurry fun (x : 𝓨) (θ : Θ) ↦
      HMul.hMul (β := ℝ≥0∞) (ℓ θ x) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))
    (μ.prod π)

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∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
inst_2 : IsMarkovKernel P
inst_3 : SFinite π
hl : Measurable (uncurry ℓ)
⊢ bayesRisk ℓ P π = ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π

Tactic:
simp [bayesRisk_of_subsingleton' hl]

Premises used: ProbabilityTheory.bayesRisk_of_subsingleton'
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst : IsMarkovKernel η
simp :
  ∀ (i : Kernel 𝓧' 𝓨) (i_1 : IsMarkovKernel i),
    ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
      ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(i ∘ₖ (η ∘ₖ P) : (a : Θ) → Measure 𝓨) θ ∂π
⊢ bayesRisk ℓ P π ≤ bayesRisk ℓ (η ∘ₖ P) π

Tactic:
simp only [bayesRisk, avgRisk, le_iInf_iff]

Premises used: ProbabilityTheory.bayesRisk, le_iInf_iff, ProbabilityTheory.avgRisk
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst : IsMarkovKernel η
κ : Kernel 𝓧' 𝓨
hκ : IsMarkovKernel κ
rw :
  ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
    ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ η ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π
⊢ ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
    ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ (η ∘ₖ P) : (a : Θ) → Measure 𝓨) θ ∂π

Tactic:
rw [← κ.comp_assoc η]

Premises used: ProbabilityTheory.Kernel.comp_assoc
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst : IsMarkovKernel η
κ : Kernel 𝓧' 𝓨
hκ : IsMarkovKernel κ
⊢ ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
    ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ η ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π

Tactic:
iInf_le_of_le (κ ∘ₖ η) (iInf_le_of_le inferInstance le_rfl)

Premises used: le_rfl, ProbabilityTheory.Kernel.comp, inferInstance, iInf_le_of_le
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst : IsMarkovKernel η
κ : Kernel 𝓧' 𝓨
hκ : IsMarkovKernel κ
⊢ ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
    ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ η ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π

Tactic:
exact iInf_le_of_le (κ ∘ₖ η) (iInf_le_of_le inferInstance le_rfl)
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
f : 𝓧 → 𝓧'
hf : Measurable f
rw : bayesRisk ℓ P π ≤ bayesRisk ℓ (Kernel.deterministic f hf ∘ₖ P) π
⊢ bayesRisk ℓ P π ≤ bayesRisk (m𝓧 := m𝓧') ℓ (P.map f) π

Tactic:
rw [← Kernel.deterministic_comp_eq_map hf]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_eq_map
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
f : 𝓧 → 𝓧'
hf : Measurable f
⊢ bayesRisk ℓ P π ≤ bayesRisk ℓ (Kernel.deterministic f hf ∘ₖ P) π

Tactic:
bayesRisk_le_bayesRisk_comp _ _ _ _

Premises used: ProbabilityTheory.bayesRisk_le_bayesRisk_comp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
f : 𝓧 → 𝓧'
hf : Measurable f
⊢ bayesRisk ℓ P π ≤ bayesRisk ℓ (Kernel.deterministic f hf ∘ₖ P) π

Tactic:
exact bayesRisk_le_bayesRisk_comp _ _ _ _

Premises used: ProbabilityTheory.bayesRisk_le_bayesRisk_comp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst_1 : IsMarkovKernel η
⊢ Measurable (α := 𝓧 × 𝓧') Prod.fst

Tactic:
fun_prop
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst_1 : IsMarkovKernel η
rw : P = (P ⊗ₖ η).map Prod.fst
rw₁ : P = (P ⊗ₖ η).fst
rw₂ rw₃ : P = P
⊢ P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)

Tactic:
rw [Kernel.deterministic_comp_eq_map, ← Kernel.fst_eq, Kernel.fst_compProd]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_eq_map, ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.Kernel.fst_compProd
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst_1 : IsMarkovKernel η
⊢ P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)

Tactic:
have : P = (Kernel.deterministic Prod.fst (by fun_prop)) ∘ₖ (P ⊗ₖ η) := by
    rw [Kernel.deterministic_comp_eq_map, ← Kernel.fst_eq, Kernel.fst_compProd]
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst_1 : IsMarkovKernel η
this : P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)
nth_rw : bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ (Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)) π
⊢ bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ P π

Tactic:
nth_rw 2 [this]
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst_1 : IsMarkovKernel η
this : P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)
⊢ bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ (Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)) π

Tactic:
bayesRisk_le_bayesRisk_comp _ _ _ _

Premises used: ProbabilityTheory.bayesRisk_le_bayesRisk_comp
-- Module: Mathlib.Probability.Decision.Risk.Basic
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst_1 : IsMarkovKernel η
this : P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)
⊢ bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ (Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)) π

Tactic:
exact bayesRisk_le_bayesRisk_comp _ _ _ _

Premises used: ProbabilityTheory.bayesRisk_le_bayesRisk_comp
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
κ : Kernel 𝓧 𝓨
π : Measure Θ
⊢ avgRisk ℓ 0 κ π = 0

Tactic:
simp [avgRisk]

Premises used: ProbabilityTheory.avgRisk
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
⊢ avgRisk (m𝓨 := m𝓨) ℓ P 0 π = 0

Tactic:
simp [avgRisk]

Premises used: ProbabilityTheory.avgRisk
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
⊢ avgRisk ℓ P κ 0 = 0

Tactic:
simp [avgRisk]

Premises used: ProbabilityTheory.avgRisk
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst : Nonempty 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
π : Measure Θ
⊢ bayesRisk.{u_1, u_2, u_3} (𝓧 := 𝓧) (m𝓧 := m𝓧) ℓ 0 π = 0

Tactic:
simp [bayesRisk, iInf_subtype']

Premises used: ProbabilityTheory.bayesRisk, iInf_subtype'
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst : Nonempty 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
⊢ bayesRisk ℓ P 0 = 0

Tactic:
simp [bayesRisk, iInf_subtype']

Premises used: ProbabilityTheory.bayesRisk, iInf_subtype'
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst : Nonempty 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
⊢ minimaxRisk.{u_1, u_2, u_3} (𝓧 := 𝓧) (mΘ := mΘ) (m𝓧 := m𝓧) ℓ 0 = 0

Tactic:
simp [minimaxRisk, iInf_subtype']

Premises used: ProbabilityTheory.minimaxRisk, iInf_subtype'
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst : IsEmpty 𝓧
⊢ avgRisk ℓ P κ π = 0

Tactic:
simp [Subsingleton.elim P 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst : IsEmpty 𝓨
⊢ avgRisk ℓ P κ π = 0

Tactic:
simp [Subsingleton.elim κ 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst : IsEmpty Θ
⊢ avgRisk ℓ P κ π = 0

Tactic:
simp [avgRisk]

Premises used: ProbabilityTheory.avgRisk
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : IsEmpty 𝓧
⊢ bayesRisk ℓ P π = 0

Tactic:
simp [bayesRisk]

Premises used: ProbabilityTheory.bayesRisk
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
simp : ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x
⊢ IsEmpty (Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel)

Tactic:
simp only [isEmpty_subtype]

Premises used: isEmpty_subtype
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x

Tactic:
fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero

Premises used: ProbabilityTheory.Kernel.not_isMarkovKernel_zero, Eq.rec, Subsingleton.elim, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x

Tactic:
exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ IsEmpty (Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel)

Tactic:
have : IsEmpty (Subtype (@IsMarkovKernel 𝓧 𝓨 m𝓧 m𝓨)) := by
    simp only [isEmpty_subtype]
    exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
this : IsEmpty (Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel)
⊢ bayesRisk ℓ P π = ∞

Tactic:
simp [bayesRisk, iInf_subtype']

Premises used: ProbabilityTheory.bayesRisk, iInf_subtype'
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : IsEmpty Θ
inst_1 : Nonempty 𝓨
⊢ bayesRisk ℓ P π = 0

Tactic:
simp [bayesRisk, iInf_subtype']

Premises used: ProbabilityTheory.bayesRisk, iInf_subtype'
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsEmpty 𝓧
⊢ minimaxRisk ℓ P = 0

Tactic:
simp [minimaxRisk, Subsingleton.elim P 0]

Premises used: ProbabilityTheory.minimaxRisk, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
simp : ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x
⊢ IsEmpty (Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel)

Tactic:
simp only [isEmpty_subtype]

Premises used: isEmpty_subtype
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x

Tactic:
fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero

Premises used: ProbabilityTheory.Kernel.not_isMarkovKernel_zero, Eq.rec, Subsingleton.elim, OfNat.ofNat, Eq.symm