Simple Bayesian binary hypothesis testing

Main definitions

• simpleBinaryLoss: the 0-1 loss on Bool, ℓ(y, z) = 𝕀{y ≠ z}.
• bayesBinaryRisk μ ν π: the Bayes risk of the simple binary hypothesis testing problem between μ and ν with respect to the prior π.

Main statements

• bayesBinaryRisk_le_bayesBinaryRisk_comp: data-processing inequality.
• bayesBinaryRisk_eq_lintegral_min: formula for the Bayes binary risk as an integral.

noncomputable def ProbabilityTheory.simpleBinaryLoss (y z : Bool) : ENNReal

The loss of the simple binary hypothesis testing problem: ℓ(y, z) = 𝕀{y ≠ z}.

Equations

• ProbabilityTheory.simpleBinaryLoss y z = if y = z then 0 else 1

@[simp]

theorem ProbabilityTheory.simpleBinaryLoss_self (y : Bool) : simpleBinaryLoss y y = 0

@[simp]

theorem ProbabilityTheory.simpleBinaryLoss_true_false : simpleBinaryLoss true false = 1

@[simp]

theorem ProbabilityTheory.simpleBinaryLoss_false_true : simpleBinaryLoss false true = 1

theorem ProbabilityTheory.measurable_simpleBinaryLoss : Measurable (Function.uncurry simpleBinaryLoss)

@[simp]

theorem ProbabilityTheory.lintegral_simpleBinaryLoss_true (ξ : MeasureTheory.Measure Bool) : ∫⁻ (z : Bool), simpleBinaryLoss true z ∂ξ = ξ {false}

@[simp]

theorem ProbabilityTheory.lintegral_simpleBinaryLoss_false (ξ : MeasureTheory.Measure Bool) : ∫⁻ (z : Bool), simpleBinaryLoss false z ∂ξ = ξ {true}

noncomputable def ProbabilityTheory.binaryGenBayesEstimator {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : 𝒳 → Bool

The function x ↦ 𝕀{π₀ * ∂μ/∂(boolKernel μ ν ∘ₘ π) x ≤ π₁ * ∂ν/∂(boolKernel μ ν ∘ₘ π) x}. It is an argmin estimator for the simple binary hypothesis testing problem.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.isArgminEstimator_binaryGenBayesEstimator {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : IsArgminEstimator simpleBinaryLoss (Kernel.boolKernel μ ν) π (binaryGenBayesEstimator μ ν π)

theorem ProbabilityTheory.hasArgminEstimator_simpleBinaryLoss {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : HasArgminEstimator simpleBinaryLoss (Kernel.boolKernel μ ν) π

theorem ProbabilityTheory.bayesRisk_boolKernel_eq_lintegral_iInf {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {𝒴 : Type u_3} [MeasurableSpace 𝒴] {ℓ : Bool → 𝒴 → ENNReal} (hℓ : Measurable (Function.uncurry ℓ)) (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] (h : HasArgminEstimator ℓ (Kernel.boolKernel μ ν) π) : bayesRisk ℓ (Kernel.boolKernel μ ν) π = ∫⁻ (x : 𝒳), ⨅ (y : 𝒴), π {true} * ν.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x * ℓ true y + π {false} * μ.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x * ℓ false y ∂π.bind ⇑(Kernel.boolKernel μ ν)

The Bayes risk for a prior π of an estimation problem with parameter space Bool and data generating kernel boolKernel μ ν, when it admits an argmin estimator.

noncomputable def ProbabilityTheory.bayesBinaryRisk {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : ENNReal

The Bayes risk of simple binary hypothesis testing with respect to a prior.

Equations

• ProbabilityTheory.bayesBinaryRisk μ ν π = ProbabilityTheory.bayesRisk ProbabilityTheory.simpleBinaryLoss (ProbabilityTheory.Kernel.boolKernel μ ν) π

theorem ProbabilityTheory.bayesBinaryRisk_eq {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : bayesBinaryRisk μ ν π = ⨅ (κ : Kernel 𝒳 Bool), ⨅ (_ : IsMarkovKernel κ), π {true} * (ν.bind ⇑κ) {false} + π {false} * (μ.bind ⇑κ) {true}

theorem ProbabilityTheory.bayesBinaryRisk_smul_smul {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) (a b : ENNReal) : bayesBinaryRisk (a • μ) (b • ν) π = bayesBinaryRisk μ ν (π.withDensity fun (x : Bool) => bif x then b else a)

B (a•μ, b•ν; π) = B (μ, ν; (a*π₀, b*π₁)).

theorem ProbabilityTheory.bayesBinaryRisk_eq_bayesBinaryRisk_one_one {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : bayesBinaryRisk μ ν π = bayesBinaryRisk (π {false} • μ) (π {true} • ν) (Bool.boolMeasure 1 1)

theorem ProbabilityTheory.bayesBinaryRisk_le_bayesBinaryRisk_comp {𝒳 : Type u_1} {𝒳' : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {m𝒳' : MeasurableSpace 𝒳'} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) (η : Kernel 𝒳 𝒳') [IsMarkovKernel η] : bayesBinaryRisk μ ν π ≤ bayesBinaryRisk (μ.bind ⇑η) (ν.bind ⇑η) π

Data processing inequality for the Bayes binary risk.

@[simp]

theorem ProbabilityTheory.bayesBinaryRisk_self {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : bayesBinaryRisk μ μ π = min (π {false}) (π {true}) * μ Set.univ

theorem ProbabilityTheory.bayesBinaryRisk_dirac {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (a b : ENNReal) (x : 𝒳) (π : MeasureTheory.Measure Bool) : bayesBinaryRisk (a • MeasureTheory.Measure.dirac x) (b • MeasureTheory.Measure.dirac x) π = min (π {false} * a) (π {true} * b)

theorem ProbabilityTheory.bayesBinaryRisk_le_min {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : bayesBinaryRisk μ ν π ≤ min (π {false} * μ Set.univ) (π {true} * ν Set.univ)

@[simp]

theorem ProbabilityTheory.bayesBinaryRisk_zero_left {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} : bayesBinaryRisk 0 ν π = 0

@[simp]

theorem ProbabilityTheory.bayesBinaryRisk_zero_right {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} : bayesBinaryRisk μ 0 π = 0

@[simp]

theorem ProbabilityTheory.bayesBinaryRisk_zero_prior {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ ν : MeasureTheory.Measure 𝒳} : bayesBinaryRisk μ ν 0 = 0

theorem ProbabilityTheory.bayesBinaryRisk_ne_top {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : bayesBinaryRisk μ ν π ≠ ⊤

theorem ProbabilityTheory.bayesBinaryRisk_of_measure_true_eq_zero {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure 𝒳) (hπ : π {true} = 0) : bayesBinaryRisk μ ν π = 0

theorem ProbabilityTheory.bayesBinaryRisk_of_measure_false_eq_zero {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure 𝒳) (hπ : π {false} = 0) : bayesBinaryRisk μ ν π = 0

theorem ProbabilityTheory.bayesBinaryRisk_symm {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : bayesBinaryRisk μ ν π = bayesBinaryRisk ν μ (MeasureTheory.Measure.map not π)

theorem ProbabilityTheory.avgRisk_binary_of_deterministic_indicator {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) {E : Set 𝒳} (hE : MeasurableSet E) : avgRisk simpleBinaryLoss (Kernel.boolKernel μ ν) (Kernel.deterministic (fun (x : 𝒳) => Bool.ofNat (E.indicator 1 x)) ⋯) π = π {false} * μ E + π {true} * ν Eᶜ

theorem ProbabilityTheory.bayesBinaryRisk_eq_iInf_measurableSet {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : bayesBinaryRisk μ ν π = ⨅ (E : Set 𝒳), ⨅ (_ : MeasurableSet E), π {false} * μ E + π {true} * ν Eᶜ

theorem ProbabilityTheory.bayesBinaryRisk_eq_lintegral_min {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : bayesBinaryRisk μ ν π = ∫⁻ (x : 𝒳), min (π {false} * μ.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x) (π {true} * ν.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x) ∂π.bind ⇑(Kernel.boolKernel μ ν)

theorem ProbabilityTheory.toReal_bayesBinaryRisk_eq_integral_min {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : (bayesBinaryRisk μ ν π).toReal = ∫ (x : 𝒳), min (π {false} * μ.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x).toReal (π {true} * ν.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x).toReal ∂π.bind ⇑(Kernel.boolKernel μ ν)

theorem ProbabilityTheory.toReal_bayesBinaryRisk_eq_integral_abs {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : (bayesBinaryRisk μ ν π).toReal = 2⁻¹ * (((π.bind ⇑(Kernel.boolKernel μ ν)) Set.univ).toReal - ∫ (x : 𝒳), |(π {false} * μ.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x).toReal - (π {true} * ν.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x).toReal| ∂π.bind ⇑(Kernel.boolKernel μ ν))

theorem ProbabilityTheory.bayesBinaryRisk_eq_lintegral_ennnorm {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : bayesBinaryRisk μ ν π = 2⁻¹ * ((π.bind ⇑(Kernel.boolKernel μ ν)) Set.univ - ∫⁻ (x : 𝒳), ↑‖(π {false} * μ.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x).toReal - (π {true} * ν.rnDeriv (π.bind ⇑(Kernel.boolKernel μ ν)) x).toReal‖₊ ∂π.bind ⇑(Kernel.boolKernel μ ν))