theorem
ProbabilityTheory.estimationProblem.ext
{Θ : Type u_8}
{𝒴 : Type u_9}
{𝒵 : Type u_10}
:
∀ {inst : MeasurableSpace Θ} {inst_1 : MeasurableSpace 𝒴} {inst_2 : MeasurableSpace 𝒵}
{x y : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}, x.y = y.y → x.ℓ = y.ℓ → x = y
theorem
ProbabilityTheory.estimationProblem.ext_iff
{Θ : Type u_8}
{𝒴 : Type u_9}
{𝒵 : Type u_10}
:
∀ {inst : MeasurableSpace Θ} {inst_1 : MeasurableSpace 𝒴} {inst_2 : MeasurableSpace 𝒵}
{x y : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}, x = y ↔ x.y = y.y ∧ x.ℓ = y.ℓ
structure
ProbabilityTheory.estimationProblem
(Θ : Type u_8)
(𝒴 : Type u_9)
(𝒵 : Type u_10)
[MeasurableSpace Θ]
[MeasurableSpace 𝒴]
[MeasurableSpace 𝒵]
:
Type (max (max u_10 u_8) u_9)
An estimation problem: a kernel P from a parameter space Θ to a sample space 𝒳,
an objective function y on the parameter space and a cost function ℓ.
We don't put the data generating kernel into this structure, since we will often perform operations
on it and we don't want to duplicate all kernel operations on estimationProblem.
- y : Θ → 𝒴
The objective function.
- y_meas : Measurable self.y
The cost (or loss) function.
- ℓ_meas : Measurable self.ℓ
Instances For
theorem
ProbabilityTheory.estimationProblem.y_meas
{Θ : Type u_8}
{𝒴 : Type u_9}
{𝒵 : Type u_10}
[MeasurableSpace Θ]
[MeasurableSpace 𝒴]
[MeasurableSpace 𝒵]
(self : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
:
Measurable self.y
theorem
ProbabilityTheory.estimationProblem.ℓ_meas
{Θ : Type u_8}
{𝒴 : Type u_9}
{𝒵 : Type u_10}
[MeasurableSpace Θ]
[MeasurableSpace 𝒴]
[MeasurableSpace 𝒵]
(self : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
:
Measurable self.ℓ
@[simp]
theorem
ProbabilityTheory.estimationProblem.comap_ℓ
{Θ : Type u_1}
{Θ' : Type u_2}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{mΘ' : MeasurableSpace Θ'}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(f : Θ' → Θ)
(hf : Measurable f)
:
@[simp]
theorem
ProbabilityTheory.estimationProblem.comap_y
{Θ : Type u_1}
{Θ' : Type u_2}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{mΘ' : MeasurableSpace Θ'}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(f : Θ' → Θ)
(hf : Measurable f)
:
noncomputable def
ProbabilityTheory.estimationProblem.comap
{Θ : Type u_1}
{Θ' : Type u_2}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{mΘ' : MeasurableSpace Θ'}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(f : Θ' → Θ)
(hf : Measurable f)
:
Given an estimation problem E and a measurable function f : Θ' → Θ, we can consider a new
estimation problem where the kernel is given by the pullback of E.P through f.
Instances For
noncomputable def
ProbabilityTheory.risk
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
(θ : Θ)
:
The risk of an estimator κ on an estimation problem E with data generating kernel P
at the parameter θ.
Equations
- ProbabilityTheory.risk E P κ θ = ∫⁻ (z : 𝒵), E.ℓ (E.y θ, z) ∂(κ.comp P) θ
Instances For
noncomputable def
ProbabilityTheory.bayesianRisk
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
(π : MeasureTheory.Measure Θ)
:
The bayesian risk of an estimator κ on an estimation problem E with data generating
kernel P with respect to a prior π.
Equations
- ProbabilityTheory.bayesianRisk E P κ π = ∫⁻ (θ : Θ), ProbabilityTheory.risk E P κ θ ∂π
Instances For
@[simp]
theorem
ProbabilityTheory.bayesianRisk_of_isEmpty
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
{P : ProbabilityTheory.Kernel Θ 𝒳}
{κ : ProbabilityTheory.Kernel 𝒳 𝒵}
{π : MeasureTheory.Measure Θ}
{E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}
[IsEmpty Θ]
:
ProbabilityTheory.bayesianRisk E P κ π = 0
theorem
ProbabilityTheory.bayesianRisk_le_iSup_risk
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsProbabilityMeasure π]
:
ProbabilityTheory.bayesianRisk E P κ π ≤ ⨆ (θ : Θ), ProbabilityTheory.risk E P κ θ
theorem
ProbabilityTheory.bayesianRisk_comap_measurableEquiv
{Θ : Type u_1}
{Θ' : Type u_2}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{mΘ' : MeasurableSpace Θ'}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsSFiniteKernel P]
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
[ProbabilityTheory.IsSFiniteKernel κ]
(π : MeasureTheory.Measure Θ)
(e : Θ ≃ᵐ Θ')
:
ProbabilityTheory.bayesianRisk (E.comap ⇑e.symm ⋯) (P.comap ⇑e.symm ⋯) κ (MeasureTheory.Measure.map (⇑e) π) = ProbabilityTheory.bayesianRisk E P κ π
noncomputable def
ProbabilityTheory.bayesRiskPrior
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
:
The Bayes risk of an estimation problem E with respect to a prior π, defined as the infimum
of the Bayesian risks of all estimators.
Equations
- ProbabilityTheory.bayesRiskPrior E P π = ⨅ (κ : ProbabilityTheory.Kernel 𝒳 𝒵), ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ProbabilityTheory.bayesianRisk E P κ π
Instances For
theorem
ProbabilityTheory.bayesRiskPrior_le_bayesRiskPrior_comp
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒳' : Type u_4}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
(η : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.bayesRiskPrior E P π ≤ ProbabilityTheory.bayesRiskPrior E (η.comp P) π
Data processing inequality for the Bayes risk with respect to a prior.
def
ProbabilityTheory.IsBayesEstimator
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
(π : MeasureTheory.Measure Θ)
:
An estimator is a Bayes estimator for a prior π if it attains the Bayes risk for π.
Equations
- ProbabilityTheory.IsBayesEstimator E P κ π = (ProbabilityTheory.bayesianRisk E P κ π = ProbabilityTheory.bayesRiskPrior E P π)
Instances For
noncomputable def
ProbabilityTheory.bayesRisk
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
:
The Bayes risk of an estimation problem E, defined as the supremum over priors of the Bayes
risk of E with respect to the prior.
Equations
- ProbabilityTheory.bayesRisk E P = ⨆ (π : MeasureTheory.Measure Θ), ⨆ (_ : MeasureTheory.IsProbabilityMeasure π), ProbabilityTheory.bayesRiskPrior E P π
Instances For
noncomputable def
ProbabilityTheory.minimaxRisk
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
:
The Bayes risk of an estimation problem E, defined as the infimum over estimators of the
maximal risk of the estimator.
Equations
- ProbabilityTheory.minimaxRisk E P = ⨅ (κ : ProbabilityTheory.Kernel 𝒳 𝒵), ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ⨆ (θ : Θ), ProbabilityTheory.risk E P κ θ
Instances For
theorem
ProbabilityTheory.bayesRiskPrior_le_minimaxRisk
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsProbabilityMeasure π]
:
theorem
ProbabilityTheory.bayesRisk_le_minimaxRisk
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
:
Properties of the Bayes risk of a prior #
theorem
ProbabilityTheory.bayesRiskPrior_compProd_le_bayesRiskPrior
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒳' : Type u_4}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsSFiniteKernel P]
(π : MeasureTheory.Measure Θ)
(κ : ProbabilityTheory.Kernel (Θ × 𝒳) 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.bayesRiskPrior E (P.compProd κ) π ≤ ProbabilityTheory.bayesRiskPrior E P π
theorem
ProbabilityTheory.bayesRiskPrior_le_inf
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
[ProbabilityTheory.IsMarkovKernel P]
:
ProbabilityTheory.bayesRiskPrior E P π ≤ ⨅ (z : 𝒵), ∫⁻ (θ : Θ), E.ℓ (E.y θ, z) ∂π
theorem
ProbabilityTheory.bayesianRisk_eq_lintegral_bayesInv_prod
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsFiniteKernel P]
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsFiniteMeasure π]
[ProbabilityTheory.IsSFiniteKernel κ]
:
ProbabilityTheory.bayesianRisk E P κ π = ∫⁻ (θz : Θ × 𝒵), E.ℓ (E.y θz.1, θz.2) ∂(π.bind ⇑P).bind ⇑((ProbabilityTheory.bayesInv P π).prod κ)
The Bayesian risk of an estimator κ with respect to a prior π can be expressed as
an integral in the following way: R_π(κ) = ((P†π × κ) ∘ P ∘ π)[(θ, z) ↦ ℓ(y(θ), z)].
theorem
ProbabilityTheory.bayesianRisk_eq_integral_integral_integral
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsFiniteKernel P]
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsFiniteMeasure π]
[ProbabilityTheory.IsSFiniteKernel κ]
:
ProbabilityTheory.bayesianRisk E P κ π = ∫⁻ (x : 𝒳), ∫⁻ (z : 𝒵), ∫⁻ (θ : Θ), E.ℓ (E.y θ, z) ∂(ProbabilityTheory.bayesInv P π) x ∂κ x ∂π.bind ⇑P
theorem
ProbabilityTheory.bayesianRisk_ge_lintegral_iInf_bayesInv
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsFiniteKernel P]
(κ : ProbabilityTheory.Kernel 𝒳 𝒵)
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsFiniteMeasure π]
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.bayesianRisk E P κ π ≥ ∫⁻ (x : 𝒳), ⨅ (z : 𝒵), ∫⁻ (θ : Θ), E.ℓ (E.y θ, z) ∂(ProbabilityTheory.bayesInv P π) x ∂π.bind ⇑P
Generalized Bayes estimator #
structure
ProbabilityTheory.IsGenBayesEstimator
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsFiniteKernel P]
(f : 𝒳 → 𝒵)
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsFiniteMeasure π]
:
We say that a measurable function f : 𝒳 → 𝒵 is a Generalized Bayes estimator for the
estimation problem E with respect to the prior π if for (P ∘ₘ π)-almost every x it is of
the form x ↦ argmin_z P†π(x)[θ ↦ ℓ(y(θ), z)].
- measurable : Measurable f
- property : ∀ᵐ (x : 𝒳) ∂π.bind ⇑P, ∫⁻ (θ : Θ), E.ℓ (E.y θ, f x) ∂(ProbabilityTheory.bayesInv P π) x = ⨅ (z : 𝒵), ∫⁻ (θ : Θ), E.ℓ (E.y θ, z) ∂(ProbabilityTheory.bayesInv P π) x
Instances For
theorem
ProbabilityTheory.IsGenBayesEstimator.measurable
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
{E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}
{P : ProbabilityTheory.Kernel Θ 𝒳}
[ProbabilityTheory.IsFiniteKernel P]
{f : 𝒳 → 𝒵}
{π : MeasureTheory.Measure Θ}
[MeasureTheory.IsFiniteMeasure π]
(self : ProbabilityTheory.IsGenBayesEstimator E P f π)
:
theorem
ProbabilityTheory.IsGenBayesEstimator.property
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
{E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}
{P : ProbabilityTheory.Kernel Θ 𝒳}
[ProbabilityTheory.IsFiniteKernel P]
{f : 𝒳 → 𝒵}
{π : MeasureTheory.Measure Θ}
[MeasureTheory.IsFiniteMeasure π]
(self : ProbabilityTheory.IsGenBayesEstimator E P f π)
:
∀ᵐ (x : 𝒳) ∂π.bind ⇑P,
∫⁻ (θ : Θ), E.ℓ (E.y θ, f x) ∂(ProbabilityTheory.bayesInv P π) x = ⨅ (z : 𝒵), ∫⁻ (θ : Θ), E.ℓ (E.y θ, z) ∂(ProbabilityTheory.bayesInv P π) x
@[reducible, inline]
noncomputable abbrev
ProbabilityTheory.IsGenBayesEstimator.Kernel
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
{P : ProbabilityTheory.Kernel Θ 𝒳}
{π : MeasureTheory.Measure Θ}
{E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
{f : 𝒳 → 𝒵}
[ProbabilityTheory.IsFiniteKernel P]
[MeasureTheory.IsFiniteMeasure π]
(h : ProbabilityTheory.IsGenBayesEstimator E P f π)
:
Given a Generalized Bayes estimator f, we can define a deterministic kernel.
Equations
- h.Kernel = ProbabilityTheory.Kernel.deterministic f ⋯
Instances For
theorem
ProbabilityTheory.bayesianRisk_of_isGenBayesEstimator
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
{P : ProbabilityTheory.Kernel Θ 𝒳}
{π : MeasureTheory.Measure Θ}
{E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
{f : 𝒳 → 𝒵}
[ProbabilityTheory.IsFiniteKernel P]
[MeasureTheory.IsFiniteMeasure π]
(hf : ProbabilityTheory.IsGenBayesEstimator E P f π)
:
ProbabilityTheory.bayesianRisk E P hf.Kernel π = ∫⁻ (x : 𝒳), ⨅ (z : 𝒵), ∫⁻ (θ : Θ), E.ℓ (E.y θ, z) ∂(ProbabilityTheory.bayesInv P π) x ∂π.bind ⇑P
theorem
ProbabilityTheory.isBayesEstimator_of_isGenBayesEstimator
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
{P : ProbabilityTheory.Kernel Θ 𝒳}
{π : MeasureTheory.Measure Θ}
{E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
{f : 𝒳 → 𝒵}
[ProbabilityTheory.IsFiniteKernel P]
[MeasureTheory.IsFiniteMeasure π]
(hf : ProbabilityTheory.IsGenBayesEstimator E P f π)
:
ProbabilityTheory.IsBayesEstimator E P hf.Kernel π
class
ProbabilityTheory.HasGenBayesEstimator
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsFiniteKernel P]
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsFiniteMeasure π]
:
Type (max u_3 u_7)
The estimation problem E admits a Generalized Bayes estimator with respect to
the prior π.
- estimator : 𝒳 → 𝒵
The Generalized Bayes estimator.
- property : ProbabilityTheory.IsGenBayesEstimator E P (ProbabilityTheory.HasGenBayesEstimator.estimator E P π) π
Instances
theorem
ProbabilityTheory.HasGenBayesEstimator.property
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
:
∀ {inst : StandardBorelSpace Θ} {inst_1 : Nonempty Θ} {E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵}
{P : ProbabilityTheory.Kernel Θ 𝒳} {inst_2 : ProbabilityTheory.IsFiniteKernel P} {π : MeasureTheory.Measure Θ}
{inst_3 : MeasureTheory.IsFiniteMeasure π} [self : ProbabilityTheory.HasGenBayesEstimator E P π],
ProbabilityTheory.IsGenBayesEstimator E P (ProbabilityTheory.HasGenBayesEstimator.estimator E P π) π
theorem
ProbabilityTheory.bayesRiskPrior_eq_of_hasGenBayesEstimator
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
[StandardBorelSpace Θ]
[Nonempty Θ]
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
[ProbabilityTheory.IsFiniteKernel P]
(π : MeasureTheory.Measure Θ)
[MeasureTheory.IsFiniteMeasure π]
[h : ProbabilityTheory.HasGenBayesEstimator E P π]
:
ProbabilityTheory.bayesRiskPrior E P π = ∫⁻ (x : 𝒳), ⨅ (z : 𝒵), ∫⁻ (θ : Θ), E.ℓ (E.y θ, z) ∂(ProbabilityTheory.bayesInv P π) x ∂π.bind ⇑P
Bayes risk increase #
noncomputable def
ProbabilityTheory.bayesRiskIncrease
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒳' : Type u_4}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
(η : ProbabilityTheory.Kernel 𝒳 𝒳')
:
The Bayes risk increase of an estimation problem E with respect to a prior π and a kernel
η gives us how much the composition with η increases the risk of E with respect to π.
Equations
- ProbabilityTheory.bayesRiskIncrease E P π η = ProbabilityTheory.bayesRiskPrior E (η.comp P) π - ProbabilityTheory.bayesRiskPrior E P π
Instances For
theorem
ProbabilityTheory.bayesRiskIncrease_comp
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒳' : Type u_4}
{𝒳'' : Type u_5}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{m𝒳'' : MeasurableSpace 𝒳''}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
(κ : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
(η : ProbabilityTheory.Kernel 𝒳' 𝒳'')
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.bayesRiskIncrease E P π (η.comp κ) = ProbabilityTheory.bayesRiskIncrease E P π κ + ProbabilityTheory.bayesRiskIncrease E (κ.comp P) π η
theorem
ProbabilityTheory.le_bayesRiskIncrease_comp
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒳' : Type u_4}
{𝒳'' : Type u_5}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{m𝒳'' : MeasurableSpace 𝒳''}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
(κ : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
(η : ProbabilityTheory.Kernel 𝒳' 𝒳'')
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.bayesRiskIncrease E (κ.comp P) π η ≤ ProbabilityTheory.bayesRiskIncrease E P π (η.comp κ)
theorem
ProbabilityTheory.bayesRiskIncrease_discard_comp_le_bayesRiskIncrease
{Θ : Type u_1}
{𝒳 : Type u_3}
{𝒳' : Type u_4}
{𝒴 : Type u_6}
{𝒵 : Type u_7}
{mΘ : MeasurableSpace Θ}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{m𝒴 : MeasurableSpace 𝒴}
{m𝒵 : MeasurableSpace 𝒵}
(E : ProbabilityTheory.estimationProblem Θ 𝒴 𝒵)
(P : ProbabilityTheory.Kernel Θ 𝒳)
(π : MeasureTheory.Measure Θ)
(κ : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.bayesRiskIncrease E (κ.comp P) π (ProbabilityTheory.Kernel.discard 𝒳') ≤ ProbabilityTheory.bayesRiskIncrease E P π (ProbabilityTheory.Kernel.discard 𝒳)
Data processing inequality for the Bayes risk increase.