Simple Bayesian binary hypothesis testing

Main definitions

• simpleBinaryHypTest

Main statements

• fooBar_unique

Notation

Implementation details

@[simp]

theorem ProbabilityTheory.simpleBinaryHypTest_ℓ : ∀ (x : Bool × Bool), ProbabilityTheory.simpleBinaryHypTest.ℓ x = match x with | (y, z) => if y = z then 0 else 1

@[simp]

theorem ProbabilityTheory.simpleBinaryHypTest_y (a : Bool) : ProbabilityTheory.simpleBinaryHypTest.y a = id a

noncomputable def ProbabilityTheory.simpleBinaryHypTest : ProbabilityTheory.estimationProblem Bool Bool Bool

Simple binary hypothesis testing problem: a testing problem where Θ = 𝒴 = 𝒵 = {0,1}, y is the identity and the loss is ℓ(y₀, z) = 𝕀{y₀ ≠ z}.

Equations

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

@[simp]

theorem ProbabilityTheory.risk_simpleBinaryHypTest_true {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (κ : ProbabilityTheory.Kernel 𝒳 Bool) : ProbabilityTheory.risk ProbabilityTheory.simpleBinaryHypTest (ProbabilityTheory.twoHypKernel μ ν) κ true = (ν.bind ⇑κ) {false}

@[simp]

theorem ProbabilityTheory.risk_simpleBinaryHypTest_false {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (κ : ProbabilityTheory.Kernel 𝒳 Bool) : ProbabilityTheory.risk ProbabilityTheory.simpleBinaryHypTest (ProbabilityTheory.twoHypKernel μ ν) κ false = (μ.bind ⇑κ) {true}

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

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

Equations

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

theorem ProbabilityTheory.binaryGenBayesEstimator_isGenBayesEstimator {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : ProbabilityTheory.IsGenBayesEstimator ProbabilityTheory.simpleBinaryHypTest (ProbabilityTheory.twoHypKernel μ ν) (ProbabilityTheory.binaryGenBayesEstimator μ ν π) π

noncomputable instance ProbabilityTheory.instHasGenBayesEstimatorBoolSimpleBinaryHypTestTwoHypKernel {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : ProbabilityTheory.HasGenBayesEstimator ProbabilityTheory.simpleBinaryHypTest (ProbabilityTheory.twoHypKernel μ ν) π

Equations

• ProbabilityTheory.instHasGenBayesEstimatorBoolSimpleBinaryHypTestTwoHypKernel μ ν π = { estimator := ProbabilityTheory.binaryGenBayesEstimator μ ν π, property := ⋯ }

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

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

Equations

• ProbabilityTheory.bayesBinaryRisk μ ν π = ProbabilityTheory.bayesRiskPrior ProbabilityTheory.simpleBinaryHypTest (ProbabilityTheory.twoHypKernel μ ν) π

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

theorem ProbabilityTheory.bayesBinaryRisk_smul_smul {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) (a : ENNReal) (b : ENNReal) : ProbabilityTheory.bayesBinaryRisk (a • μ) (b • ν) π = ProbabilityTheory.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_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : ProbabilityTheory.bayesBinaryRisk μ ν π = ProbabilityTheory.bayesBinaryRisk (π {false} • μ) (π {true} • ν) (Bool.boolMeasure 1 1)

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

Data processing inequality for the Bayes binary risk.

theorem ProbabilityTheory.nonempty_subtype_isMarkovKernel_of_nonempty {𝒳 : Type u_6} {m𝒳 : MeasurableSpace 𝒳} {𝒴 : Type u_7} {m𝒴 : MeasurableSpace 𝒴} [Nonempty 𝒴] : Nonempty (Subtype ProbabilityTheory.IsMarkovKernel)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem ProbabilityTheory.bayesianRisk_binary_of_deterministic_indicator {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) {E : Set 𝒳} (hE : MeasurableSet E) : ProbabilityTheory.bayesianRisk ProbabilityTheory.simpleBinaryHypTest (ProbabilityTheory.twoHypKernel μ ν) (ProbabilityTheory.Kernel.deterministic (fun (x : 𝒳) => Bool.ofNat (E.indicator 1 x)) ⋯) π = π {false} * μ E + π {true} * ν Eᶜ

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

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

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

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

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