Event-level likelihood ratios of two measures

The likelihood ratio μ e / ν e of a pair of measures at an event: the Bayes factor of the evidence e for the simple binary testing problem (μ, ν). Mathlib's MeasureTheory.llr is the pointwise log-ratio log (μ.rnDeriv ν x).toReal; this file's ratio is its event-level companion — the marginal likelihood ratio a Bayes factor compares, which agrees with exp (llr μ ν x) at positive-mass atoms of a discrete space and is the object Merin-style argumentation semantics needs (evidence is a proposition, not a sample point). In the vocabulary of Degenne's testing-lower-bounds development (upstreaming into Mathlib.Probability.Decision), the pair (μ, ν) is twoHypKernel μ ν; this file proves the ratio's algebra without any packaging. [UPSTREAM] candidates.

Main results

• likelihoodRatio_mul_swap: LR(μ,ν) · LR(ν,μ) = 1 at events of nonzero finite mass under both measures.
• log_likelihoodRatio: the log-ratio is a difference of surprisals.
• likelihoodRatio_inter: under independence in both measures, the ratio is multiplicative over intersections.
• max_likelihoodRatio_lt_inter, likelihoodRatio_union_lt_max, one_lt_likelihoodRatio_union: for probability measures with both events of ratio above one, intersection beats both events beats union beats one.

noncomputable def ProbabilityTheory.likelihoodRatio {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.Measure Ω) (e : Set Ω) : ENNReal

The likelihood ratio of two measures at an event, in ℝ≥0∞: total division gives the boundary cases their true values — ν e = 0 < μ e is infinitely strong evidence for μ, and 0/0 = 0.

Equations

• ProbabilityTheory.likelihoodRatio μ ν e = μ e / ν e

theorem ProbabilityTheory.likelihoodRatio_def {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.Measure Ω) (e : Set Ω) : likelihoodRatio μ ν e = μ e / ν e

theorem ProbabilityTheory.likelihoodRatio_mul_swap {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} {e : Set Ω} (hμ0 : μ e ≠ 0) (hμt : μ e ≠ ⊤) (hν0 : ν e ≠ 0) (hνt : ν e ≠ ⊤) : likelihoodRatio μ ν e * likelihoodRatio ν μ e = 1

Swapping the hypotheses inverts the ratio: LR(μ,ν) · LR(ν,μ) = 1 at any event with nonzero finite mass under both.

theorem ProbabilityTheory.log_likelihoodRatio {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} {e : Set Ω} (hμ0 : μ e ≠ 0) (hμt : μ e ≠ ⊤) (hν0 : ν e ≠ 0) (hνt : ν e ≠ ⊤) : Real.log (likelihoodRatio μ ν e).toReal = -Real.log (ν e).toReal - -Real.log (μ e).toReal

The log-likelihood ratio is a difference of surprisals: log LR(μ,ν)(E) = (−log ν E) − (−log μ E).

theorem ProbabilityTheory.likelihoodRatio_inter {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} {a b : Set Ω} (h₁ : IndepSet a b μ) (h₂ : IndepSet a b ν) (hνb0 : ν b ≠ 0) (hνbt : ν b ≠ ⊤) : likelihoodRatio μ ν (a ∩ b) = likelihoodRatio μ ν a * likelihoodRatio μ ν b

Under independence in both measures, the likelihood ratio is multiplicative over intersections.

theorem ProbabilityTheory.max_likelihoodRatio_lt_inter {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} {a b : Set Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h₁ : IndepSet a b μ) (h₂ : IndepSet a b ν) (ha : 1 < likelihoodRatio μ ν a) (hb : 1 < likelihoodRatio μ ν b) (hνa : ν a ≠ 0) (hνb : ν b ≠ 0) : max (likelihoodRatio μ ν a) (likelihoodRatio μ ν b) < likelihoodRatio μ ν (a ∩ b)

Intersection dominates both conjuncts: under independence in both measures, if both events have ratio above one then so does their intersection, strictly beyond either.

theorem ProbabilityTheory.likelihoodRatio_union_lt_max {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} {a b : Set Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hbm : MeasurableSet b) (h₁ : IndepSet a b μ) (h₂ : IndepSet a b ν) (ha : 1 < likelihoodRatio μ ν a) (hb : 1 < likelihoodRatio μ ν b) (hνa : ν a ≠ 0) (hνb : ν b ≠ 0) : likelihoodRatio μ ν (a ∪ b) < max (likelihoodRatio μ ν a) (likelihoodRatio μ ν b)

Under independence in both measures with both ratios above one, the union's ratio is strictly below the larger single-event ratio.

theorem ProbabilityTheory.one_lt_likelihoodRatio_union {Ω : Type u_1} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} {a b : Set Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hbm : MeasurableSet b) (h₁ : IndepSet a b μ) (h₂ : IndepSet a b ν) (ha : 1 < likelihoodRatio μ ν a) (hb : 1 < likelihoodRatio μ ν b) (hνa : ν a ≠ 0) (hνb : ν b ≠ 0) : 1 < likelihoodRatio μ ν (a ∪ b)

Under independence in both measures with both ratios above one, the union's ratio still exceeds one.