Documentation

TestingLowerBounds.Divergences.StatInfo.StatInfo

Statistical information #

Main definitions #

Main statements #

Notation #

Implementation details #

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

The statistical information of the measures μ and ν with respect to the prior π ∈ ℳ({0,1}).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ProbabilityTheory.statInfo_eq_min_sub {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) :
    ProbabilityTheory.statInfo μ ν π = min (π {false} * μ Set.univ) (π {true} * ν Set.univ) - ProbabilityTheory.bayesBinaryRisk μ ν π
    source
    theorem ProbabilityTheory.statInfo_eq_bayesRiskIncrease {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) :
    ProbabilityTheory.statInfo μ ν π = ProbabilityTheory.bayesRiskIncrease ProbabilityTheory.simpleBinaryHypTest (ProbabilityTheory.twoHypKernel μ ν) π (ProbabilityTheory.Kernel.discard 𝒳)
    source
    @[simp]
    theorem ProbabilityTheory.statInfo_zero_left {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} :
    ProbabilityTheory.statInfo 0 ν π = 0
    source
    @[simp]
    theorem ProbabilityTheory.statInfo_zero_right {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} :
    ProbabilityTheory.statInfo μ 0 π = 0
    source
    @[simp]
    theorem ProbabilityTheory.statInfo_zero_prior {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} :
    ProbabilityTheory.statInfo μ ν 0 = 0
    source
    @[simp]
    theorem ProbabilityTheory.statInfo_self {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} :
    ProbabilityTheory.statInfo μ μ π = 0
    source
    theorem ProbabilityTheory.statInfo_le_min {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} :
    ProbabilityTheory.statInfo μ ν π ≤ min (π {false} * μ Set.univ) (π {true} * ν Set.univ)
    source
    theorem ProbabilityTheory.statInfo_ne_top {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure π] :
    ProbabilityTheory.statInfo μ ν π ≠ ⊤
    source
    theorem ProbabilityTheory.statInfo_symm {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} :
    ProbabilityTheory.statInfo μ ν π = ProbabilityTheory.statInfo ν μ (MeasureTheory.Measure.map not π)
    source
    theorem ProbabilityTheory.statInfo_of_measure_true_eq_zero {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {π : MeasureTheory.Measure Bool} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (hπ : π {true} = 0) :
    ProbabilityTheory.statInfo μ ν π = 0
    source
    theorem ProbabilityTheory.statInfo_of_measure_false_eq_zero {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {π : MeasureTheory.Measure Bool} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (hπ : π {false} = 0) :
    ProbabilityTheory.statInfo μ ν π = 0
    source
    theorem ProbabilityTheory.statInfo_comp_le {𝒳 : Type u_1} {𝒳' : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {m𝒳' : MeasurableSpace 𝒳'} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) (η : ProbabilityTheory.Kernel 𝒳 𝒳') [ProbabilityTheory.IsMarkovKernel η] :
    ProbabilityTheory.statInfo (μ.bind ⇑η) (ν.bind ⇑η) π ≤ ProbabilityTheory.statInfo μ ν π

    Data processing inequality for the statistical information.

    source
    theorem ProbabilityTheory.toReal_statInfo_eq_toReal_sub {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure π] :
    (ProbabilityTheory.statInfo μ ν π).toReal = (min (π {false} * μ Set.univ) (π {true} * ν Set.univ)).toReal - (ProbabilityTheory.bayesBinaryRisk μ ν π).toReal
    source
    theorem ProbabilityTheory.statInfo_boolMeasure_le_statInfo {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} {E : Set 𝒳} (hE : MeasurableSet E) :
    ProbabilityTheory.statInfo (Bool.boolMeasure (μ Eᶜ) (μ E)) (Bool.boolMeasure (ν Eᶜ) (ν E)) π ≤ ProbabilityTheory.statInfo μ ν π
    source
    theorem ProbabilityTheory.statInfo_eq_min_sub_lintegral {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] :
    ProbabilityTheory.statInfo μ ν π = min (π {false} * μ Set.univ) (π {true} * ν Set.univ) - ∫⁻ (x : 𝒳), min (π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x) (π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x) ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)
    source
    theorem ProbabilityTheory.statInfo_eq_min_sub_lintegral' {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {ζ : MeasureTheory.Measure 𝒳} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.SigmaFinite ζ] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] (hμζ : μ.AbsolutelyContinuous ζ) (hνζ : ν.AbsolutelyContinuous ζ) :
    ProbabilityTheory.statInfo μ ν π = min (π {false} * μ Set.univ) (π {true} * ν Set.univ) - ∫⁻ (x : 𝒳), min (π {false} * μ.rnDeriv ζ x) (π {true} * ν.rnDeriv ζ x) ∂ζ
    source
    theorem ProbabilityTheory.toReal_statInfo_eq_min_sub_integral {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] :
    (ProbabilityTheory.statInfo μ ν π).toReal = min (π {false} * μ Set.univ).toReal (π {true} * ν Set.univ).toReal - ∫ (x : 𝒳), min (π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x).toReal (π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x).toReal ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)
    source
    theorem ProbabilityTheory.toReal_statInfo_eq_min_sub_integral' {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {ζ : MeasureTheory.Measure 𝒳} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.SigmaFinite ζ] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] (hμζ : μ.AbsolutelyContinuous ζ) (hνζ : ν.AbsolutelyContinuous ζ) :
    (ProbabilityTheory.statInfo μ ν π).toReal = min (π {false} * μ Set.univ).toReal (π {true} * ν Set.univ).toReal - ∫ (x : 𝒳), min (π {false} * μ.rnDeriv ζ x).toReal (π {true} * ν.rnDeriv ζ x).toReal ∂ζ
    source
    theorem ProbabilityTheory.statInfo_eq_abs_add_lintegral_abs {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] :
    ↑(ProbabilityTheory.statInfo μ ν π) = 2⁻¹ * (↑(∫⁻ (x : 𝒳), ↑‖(π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x).toReal - (π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x).toReal‖₊ ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) - ↑|(π {false} * μ Set.univ).toReal - (π {true} * ν Set.univ).toReal|)
    source
    theorem ProbabilityTheory.toReal_statInfo_eq_integral_max_of_le {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure π] (h : π {false} * μ Set.univ ≤ π {true} * ν Set.univ) :
    (ProbabilityTheory.statInfo μ ν π).toReal = ∫ (x : 𝒳), max 0 ((π {false} * μ.rnDeriv ν x).toReal - (π {true}).toReal) ∂ν + (π {false} * (μ.singularPart ν) Set.univ).toReal
    source
    theorem ProbabilityTheory.toReal_statInfo_eq_integral_max_of_ge {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} {π : MeasureTheory.Measure Bool} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure π] (h : π {true} * ν Set.univ ≤ π {false} * μ Set.univ) :
    (ProbabilityTheory.statInfo μ ν π).toReal = ∫ (x : 𝒳), max 0 ((π {true}).toReal - (π {false} * μ.rnDeriv ν x).toReal) ∂ν
    source
    theorem ProbabilityTheory.statInfo_eq_lintegral_max_of_le {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] (h : π {false} * μ Set.univ ≤ π {true} * ν Set.univ) :
    ProbabilityTheory.statInfo μ ν π = ∫⁻ (x : 𝒳), max 0 (π {false} * μ.rnDeriv ν x - π {true}) ∂ν + π {false} * (μ.singularPart ν) Set.univ
    source
    theorem ProbabilityTheory.statInfo_eq_lintegral_max_of_gt {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] (h : π {true} * ν Set.univ < π {false} * μ Set.univ) :
    ProbabilityTheory.statInfo μ ν π = ∫⁻ (x : 𝒳), max 0 (π {true} - π {false} * μ.rnDeriv ν x) ∂ν
    source
    theorem ProbabilityTheory.toReal_statInfo_eq_integral_abs {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {π : MeasureTheory.Measure Bool} [MeasureTheory.IsFiniteMeasure π] :
    (ProbabilityTheory.statInfo μ ν π).toReal = 2⁻¹ * (-|(π {false} * μ Set.univ).toReal - (π {true} * ν Set.univ).toReal| + ∫ (x : 𝒳), |(π {false} * μ.rnDeriv ν x).toReal - (π {true}).toReal| ∂ν + (π {false} * (μ.singularPart ν) Set.univ).toReal)
    source
    theorem ProbabilityTheory.statInfo_eq_min_sub_iInf_measurableSet {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] :
    ProbabilityTheory.statInfo μ ν π = min (π {false} * μ Set.univ) (π {true} * ν Set.univ) - ⨅ (E : Set 𝒳), ⨅ (_ : MeasurableSet E), π {false} * μ E + π {true} * ν Eᶜ
    source
    theorem ProbabilityTheory.integrable_statInfoFun_rnDeriv {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (β : ℝ) (γ : ℝ) (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] :
    MeasureTheory.Integrable (fun (x : 𝒳) => ProbabilityTheory.statInfoFun β γ (μ.rnDeriv ν x).toReal) ν