Risk in countable spaces

In countable spaces, we can write integrals as sums, hence we can write the average or Bayes risk with sums instead of integrals.

theorem ProbabilityTheory.avgRisk_countable {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {κ : Kernel 𝓧 𝓨} {π : MeasureTheory.Measure Θ} [Countable Θ] [MeasurableSingletonClass Θ] : avgRisk ℓ P κ π = ∑' (θ : Θ), (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}

theorem ProbabilityTheory.avgRisk_fintype {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {κ : Kernel 𝓧 𝓨} {π : MeasureTheory.Measure Θ} [Fintype Θ] [MeasurableSingletonClass Θ] : avgRisk ℓ P κ π = ∑ θ : Θ, (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}

theorem ProbabilityTheory.avgRisk_countable' {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {κ : Kernel 𝓧 𝓨} {π : MeasureTheory.Measure Θ} [Countable 𝓨] [MeasurableSingletonClass 𝓨] (hℓ : Measurable ℓ) : avgRisk ℓ P κ π = ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π

theorem ProbabilityTheory.avgRisk_fintype' {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {κ : Kernel 𝓧 𝓨} {π : MeasureTheory.Measure Θ} [Fintype 𝓨] [MeasurableSingletonClass 𝓨] (hℓ : Measurable ℓ) : avgRisk ℓ P κ π = ∑ y : 𝓨, ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π

theorem ProbabilityTheory.bayesRisk_countable {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [Countable Θ] [MeasurableSingletonClass Θ] : bayesRisk ℓ P π = ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∑' (θ : Θ), (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}

theorem ProbabilityTheory.bayesRisk_fintype {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [Fintype Θ] [MeasurableSingletonClass Θ] : bayesRisk ℓ P π = ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∑ θ : Θ, (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}

theorem ProbabilityTheory.bayesRisk_countable' {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [Countable 𝓨] [MeasurableSingletonClass 𝓨] (hℓ : Measurable ℓ) : bayesRisk ℓ P π = ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π

theorem ProbabilityTheory.bayesRisk_fintype' {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ} [Fintype 𝓨] [MeasurableSingletonClass 𝓨] (hℓ : Measurable ℓ) : bayesRisk ℓ P π = ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), ∑ y : 𝓨, ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π

theorem ProbabilityTheory.avgRisk_const_of_countable {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [Countable 𝓨] [MeasurableSingletonClass 𝓨] (hℓ : Measurable ℓ) (μ : MeasureTheory.Measure 𝓧) (κ : Kernel 𝓧 𝓨) (π : MeasureTheory.Measure Θ) : avgRisk ℓ (Kernel.const Θ μ) κ π = ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * (μ.bind ⇑κ) {y} ∂π

theorem ProbabilityTheory.avgRisk_const_of_fintype {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [Fintype 𝓨] [MeasurableSingletonClass 𝓨] (hℓ : Measurable ℓ) (μ : MeasureTheory.Measure 𝓧) (κ : Kernel 𝓧 𝓨) (π : MeasureTheory.Measure Θ) : avgRisk ℓ (Kernel.const Θ μ) κ π = ∑ y : 𝓨, ∫⁻ (θ : Θ), ℓ θ y * (μ.bind ⇑κ) {y} ∂π