Skip to content
DraconiticResearch
Search Sources API
197,768 studies31 sourcesUpdated 2 min ago
PreprintCC BY 4.0arXiv

Birnbaum's principles in Venn diagrams: Extended version with Lean verification

  • Jaime Enrique Lincovil Curivil
  • Alexandre Galvão Patriota
Open at sourcePDFDOICite

Abstract

Birnbaum's theorem states that the sufficiency and conditionality principles jointly imply, and are implied by, the likelihood principle. To enable formal certification of the results in Lean, we make the conditionality relation explicit through a finite-sample formulation based on \cite{Evans2013}. We reformulate the theorem as a statement about classes of statistical procedures that preserve statistical relations, and show that the proof reduces to the propagation of evidential equality along chains of conditionality-related inference bases (experiment--observation pairs). The main results are illustrated by Venn diagrams, and a worked finite example exhibits two pairs of inference bases: one related by conditionality but not by sufficiency, and the other related by sufficiency but not by conditionality. For finite parameter spaces with at least two points, the class of likelihood-invariant procedures with codomain [0,1] is strictly contained in the class of sufficiency-invariant procedures.

Related

  1. Empirical coordination in the finite blocklength regime: an achievability result---Extended version
    Olivier Massicot, Giulia Cervia, Maël Le Treust
    arXivPreprintCC BY 4.0Full textGeneral mathematicsarXiv
  2. Residual-Information Generalization Bounds Under Selective Privacy: Extended Version
    Amirreza Zamani, Parastoo Sadeghi, Mikael Skoglund
    arXivPreprintCC BY 4.0Full textGeneral mathematicsarXiv
  3. A new arrangement inequality (revised and extended version)
    Mohammad Javaheri
    arXivPreprintCC BY 4.0Full textGeneral mathematicsarXiv
  4. Hypercyclic and topologically transitive semigroups of composition operators (revised and extended version)
    Mohammad Javaheri
    arXivPreprintarXiv licenceFull textDynamical systemsarXiv
  5. Where Is the Truth When AI Agents Disagree? Dependence-Aware Belief Propagation for Unsupervised Truth Discovery (Extended Version)
    Laure Berti-Equille
    arXivPreprintCC BY 4.0Full textStatisticsarXiv

Cite

BibTeXRIS
BibTeX
@misc{curivil2026birnbaums,
  title = {{Birnbaum's principles in Venn diagrams: Extended version with Lean verification}},
  author = {Jaime Enrique Lincovil Curivil and Alexandre Galvão Patriota},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.26776},
  eprint = {2609.26776},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.26776},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Birnbaum's principles in Venn diagrams: Extended version with Lean verification
AU  - Jaime Enrique Lincovil Curivil
AU  - Alexandre Galvão Patriota
PY  - 2026
DA  - 2026/09/22
PB  - arXiv
DO  - 10.48550/arxiv.2609.26776
UR  - https://arxiv.org/abs/2609.26776
AB  - Birnbaum's theorem states that the sufficiency and conditionality principles jointly imply, and are implied by, the likelihood principle. To enable formal certification of the results in Lean, we make the conditionality relation explicit through a finite-sample formulation based on \cite{Evans2013}. We reformulate the theorem as a statement about classes of statistical procedures that preserve statistical relations, and show that the proof reduces to the propagation of evidential equality along chains of conditionality-related inference bases (experiment--observation pairs). The main results are illustrated by Venn diagrams, and a worked finite example exhibits two pairs of inference bases: one related by conditionality but not by sufficiency, and the other related by sufficiency but not by conditionality. For finite parameter spaces with at least two points, the class of likelihood-invariant procedures with codomain [0,1] is strictly contained in the class of sufficiency-invariant procedures.
ER  -