awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 𝓧 μ) π
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
have inr : ∀ (hX : Nonempty 𝓧),
  bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
Tactic: rcases isEmpty_or_nonempty 𝓧 with hX | hX
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 𝓧
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
have inr : ∀ (x : 𝓧), bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
Tactic: obtain x := hX.some
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 : 𝓧
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
have inr : Eq (α := ℝ≥0∞) (⨅ (x : Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel), avgRisk ℓ P (↑x : Kernel 𝓧 𝓨) π)
  (⨅ (x : Subtype (α := Measure 𝓨) IsProbabilityMeasure), avgRisk ℓ P (Kernel.const 𝓧 (↑x : Measure 𝓨)) π)
Tactic: rw [bayesRisk, iInf_subtype', iInf_subtype']
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 κ }
⊢ (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 μ }))
        κ) =
    κ
have a : ∀ (y : 𝓧) (s : Set 𝓨),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((((↑((fun (μ : { μ : Measure 𝓨 // IsProbabilityMeasure μ }) ↦
                            (Subtype.mk (p := fun (κ : Kernel 𝓧 𝓨) ↦ IsMarkovKernel κ) (Kernel.const 𝓧 (↑μ : Measure 𝓨))
                                sorry :
                              { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }))
                          ((fun (κ : { κ : Kernel 𝓧 𝓨 // IsMarkovKernel κ }) ↦
                              (Subtype.mk (p := fun (μ : Measure 𝓨) ↦ IsProbabilityMeasure μ)
                                  (((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) x) sorry :
                                { μ : Measure 𝓨 // IsProbabilityMeasure μ }))
                            κ)) :
                      Kernel 𝓧 𝓨) :
                    Kernel 𝓧 𝓨) :
                  (a : 𝓧) → Measure 𝓨)
                y :
              Measure 𝓨) :
            (a : Set 𝓨) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((((↑κ : Kernel 𝓧 𝓨) : (a : 𝓧) → Measure 𝓨) y : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 : Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel), avgRisk ℓ P (↑x : Kernel 𝓧 𝓨) π)
    (⨅ (x : Subtype (α := Measure 𝓨) IsProbabilityMeasure), avgRisk ℓ P (Kernel.const 𝓧 (↑x : Measure 𝓨)) π)
have 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 𝓨)) π)
Tactic: rw [← Equiv.iInf_comp e.symm]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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∞) ∂π
have refine : ⨅ (y : 𝓨),
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
  bayesRisk ℓ P π
Tactic: refine le_antisymm (bayesRisk_le_iInf' hl _ _) ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 ℓ)
⊢ ⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    bayesRisk ℓ P π
have 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 𝓧 μ) π)
Tactic: rw [bayesRisk_eq_iInf_measure_of_subsingleton]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 ℓ)
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)
    (⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π)
have 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) ∂π
Tactic: simp only [avgRisk_const_right', le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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) ∂π
have 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 ∂μ) ∂π
Tactic: refine fun μ hμ ↦ (iInf_le_lintegral (μ := μ) _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 μ
⊢ ∫⁻ (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 ∂μ) ∂π
have 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 ∂μ) ∂π
Tactic: rw [lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 ∂μ) ∂π
⊢ ∫⁻ (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 ∂μ) ∂π
have hf : AEMeasurable (β := ℝ≥0∞)
  (uncurry fun (x : 𝓨) (θ : Θ) ↦
    HMul.hMul (β := ℝ≥0∞) (ℓ θ x) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))
  (μ.prod π)
Tactic: rw [lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 μ
⊢ ∫⁻ (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 ∂μ) ∂π
have 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 ∂μ)
Tactic: congr with θ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 μ
θ : Θ
⊢ ∫⁻ (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 ∂μ)
have 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 ∂μ)
Tactic: rw [lintegral_mul_const _ (by fun_prop), mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 ∂μ)
⊢ ∫⁻ (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 ∂μ)
have 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 ∂μ)
Tactic: rw [lintegral_mul_const _ (by fun_prop), mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (hypothesis)
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 μ
⊢ AEMeasurable (β := ℝ≥0∞)
    (uncurry fun (x : 𝓨) (θ : Θ) ↦
      HMul.hMul (β := ℝ≥0∞) (ℓ θ x) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))
    (μ.prod π)
have this : Measurable (β := ℝ≥0∞) fun (a : Θ) ↦ (((P : (a : Θ) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ
Tactic: have := P.measurable_coe .univ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 η
⊢ bayesRisk ℓ P π ≤ bayesRisk ℓ (η ∘ₖ P) π
have simp : ∀ (i : Kernel 𝓧' 𝓨) (i_1 : IsMarkovKernel i),
  ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
    ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(i ∘ₖ (η ∘ₖ P) : (a : Θ) → Measure 𝓨) θ ∂π
Tactic: simp only [bayesRisk, avgRisk, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 𝓨) θ ∂π
have rw : ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π ≤
  ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ η ∘ₖ P : (a : Θ) → Measure 𝓨) θ ∂π
Tactic: rw [← κ.comp_assoc η]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 (m𝓧 := m𝓧') ℓ (P.map f) π
have rw : bayesRisk ℓ P π ≤ bayesRisk ℓ (Kernel.deterministic f hf ∘ₖ P) π
Tactic: rw [← Kernel.deterministic_comp_eq_map hf]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 ⊗ₖ η)
have rw : P = (P ⊗ₖ η).map Prod.fst
Tactic: rw [Kernel.deterministic_comp_eq_map, ← Kernel.fst_eq, Kernel.fst_compProd]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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
⊢ P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)
have rw₁ : P = (P ⊗ₖ η).fst
Tactic: rw [Kernel.deterministic_comp_eq_map, ← Kernel.fst_eq, Kernel.fst_compProd]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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
⊢ P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)
have rw₂ : P = P
Tactic: rw [Kernel.deterministic_comp_eq_map, ← Kernel.fst_eq, Kernel.fst_compProd]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (hypothesis)
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 η
⊢ bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ P π
have this : P = Kernel.deterministic Prod.fst sorry ∘ₖ (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]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
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 ℓ P π
have nth_rw : bayesRisk ℓ (P ⊗ₖ η) π ≤ bayesRisk ℓ (Kernel.deterministic Prod.fst sorry ∘ₖ (P ⊗ₖ η)) π
Tactic: nth_rw 2 [this]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Defs (goal)
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)
have simp : ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x
Tactic: simp only [isEmpty_subtype]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Defs (hypothesis)
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 𝓨
⊢ bayesRisk ℓ P π = ∞
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Defs (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ IsEmpty (Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel)
have simp : ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x
Tactic: simp only [isEmpty_subtype]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Defs (hypothesis)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ minimaxRisk ℓ P = ∞
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
⊢ HasPDF X ℙ μ ↔ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
have rw : AEMeasurable X ℙ ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ ↔
  HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
Tactic: rw [hasPDF_iff]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ HasPDF X ℙ μ
have refine_1 : HaveLebesgueDecomposition (map X ℙ) μ
Tactic: refine ⟨hX, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
refine_1 : HaveLebesgueDecomposition (map X ℙ) μ
⊢ HasPDF X ℙ μ
have refine_2 : map X ℙ ≪ μ
Tactic: refine ⟨hX, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ HaveLebesgueDecomposition (map X ℙ) μ
have refine_1 : (μ.withDensity f).HaveLebesgueDecomposition μ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ map X ℙ ≪ μ
have refine_2 : μ.withDensity f ≪ μ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ
have refine_1 : (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ
Tactic: rw [withDensity_congr_ae hf.ae_eq_mk]