Bayesian fine-mapping and colocalization

49 fully proved

Wakefield's approximate Bayes factor

DefinitionWakefield's approximate Bayes factor#✓fully proved

Wakefield's approximate Bayes factor: the N(0, V + W) density of the estimate b (its marginal law under the alternative β ~ N(0, W)) divided by its N(0, V) density (the null β = 0). Wakefield (2009) reports the reciprocal, null over alternative; coloc and SuSiE use this orientation, in which large values favor association. For V = 0 the null density is Mathlib's junk value 0 and so is the ratio; the theorems assume V ≠ 0.

noncomputable def wakefieldABF (V W : ℝ≥0) (b : ℝ) : ℝ :=
  gaussianPDFReal 0 (V + W) b / gaussianPDFReal 0 V b

Used by 8

Used byWakefield's Bayes factor as a density ratio of Gaussians · The regression Bayes factor is the Wakefield ABF · The ABF is the Bayes factor · Single-effect likelihood-ratio identity · Posterior inclusion probabilities of the single-effect regression · Positivity of the single-effect regression evidence · Wakefield's closed form · Positivity of Wakefield's approximate Bayes factor

TheoremWakefield's closed form#✓fully proved

With z = b / √V, ABF = √(V / (V + W)) · exp (z² W / (2 (V + W))).

theorem wakefieldABF_eq {V : ℝ≥0} (hV : V ≠ 0) (W : ℝ≥0) (b : ℝ) :
    wakefieldABF V W b =
      √((V : ℝ) / (V + W)) * exp ((b / √(V : ℝ)) ^ 2 * W / (2 * (V + W)))

Uses 1 · Used by 2

Statement usesWakefield's approximate Bayes factor

Used byThe regression Bayes factor is the Wakefield ABF · Positivity of Wakefield's approximate Bayes factor

TheoremPositivity of Wakefield's approximate Bayes factor#✓fully proved

Wakefield's ABF is strictly positive on its sampling-variance domain.

theorem wakefieldABF_pos {V : ℝ≥0} (hV : V ≠ 0) (W : ℝ≥0) (b : ℝ) :
    0 < wakefieldABF V W b

Uses 2 · Used by 1

Statement usesWakefield's approximate Bayes factor

Proof usesWakefield's closed form

Used byPositivity of the single-effect regression evidence

TheoremWakefield's Bayes factor as a density ratio of Gaussians#✓fully proved

The alternative marginal N(0, V + W) has density wakefieldABF V W with respect to the null law N(0, V).

theorem gaussianReal_eq_withDensity_wakefieldABF {V : ℝ≥0} (hV : V ≠ 0) (W : ℝ≥0) :
    gaussianReal 0 (V + W) =
      (gaussianReal 0 V).withDensity fun b => ENNReal.ofReal (wakefieldABF V W b)

Uses 1 · Used by 1

Statement usesWakefield's approximate Bayes factor

Used byThe ABF is the Bayes factor

TheoremThe ABF is the Bayes factor#✓fully proved

If β ~ N(0, W) and the sampling error ε ~ N(0, V) are independent, the law of the estimate β + ε (alternative) has density wakefieldABF V W with respect to the law of ε (null).

theorem rnDeriv_map_add_ae_eq {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    [IsProbabilityMeasure P] {β ε : Ω → ℝ} (hβ : Measurable β) (hε : Measurable ε)
    (hind : IndepFun β ε P) {V W : ℝ≥0} (hV : V ≠ 0) (hβl : P.map β = gaussianReal 0 W)
    (hεl : P.map ε = gaussianReal 0 V) :
    (P.map (fun ω => β ω + ε ω)).rnDeriv (P.map ε) =ᵐ[P.map ε]
      fun b => ENNReal.ofReal (wakefieldABF V W b)

Uses 2

Statement usesWakefield's approximate Bayes factor

Proof usesWakefield's Bayes factor as a density ratio of Gaussians

Single-effect regression

DefinitionMarginal least-squares effect estimate#✓fully proved

The marginal least-squares effect estimate xᵀ y / xᵀ x of a variant with genotype vector x.

noncomputable def olsEffect (x y : EuclideanSpace ℝ n) : ℝ := ⟪x, y⟫ / ‖x‖ ^ 2

Used by 5

Used byThe effect posterior of the single-effect regression · The regression Bayes factor is the Wakefield ABF · Single-effect likelihood-ratio identity · Posterior inclusion probabilities of the single-effect regression · Positivity of the single-effect regression evidence

DefinitionSampling variance of the least-squares effect estimate#✓fully proved

The sampling variance σ² / xᵀ x of olsEffect x y for residual variance σ².

noncomputable def olsVar (σ2 : ℝ≥0) (x : EuclideanSpace ℝ n) : ℝ≥0 := σ2 / ‖x‖₊ ^ 2

Used by 5

Used byThe effect posterior of the single-effect regression · The regression Bayes factor is the Wakefield ABF · Single-effect likelihood-ratio identity · Posterior inclusion probabilities of the single-effect regression · Positivity of the single-effect regression evidence

DefinitionCovariance of the single-effect regression model#✓fully proved

The covariance σ₀² x xᵀ + σ² I of y = x β + e for β ~ N(0, σ₀²) and e ~ N(0, σ² I).

noncomputable def serCov (σ2 σ02 : ℝ≥0) (x : EuclideanSpace ℝ n) : Matrix n n ℝ :=
  replicateCol Unit (ofLp x) * ((σ02 : ℝ) • (1 : Matrix Unit Unit ℝ)) *
      (replicateCol Unit (ofLp x))ᵀ + (σ2 : ℝ) • (1 : Matrix n n ℝ)

Used by 6

Used byThe effect posterior of the single-effect regression · The marginal law of the phenotype given the causal variant · The regression Bayes factor is the Wakefield ABF · Single-effect regression covariance is positive definite · Single-effect likelihood-ratio identity · Posterior inclusion probabilities of the single-effect regression

TheoremSingle-effect regression covariance is positive definite#✓fully proved

serCov σ2 σ02 x is positive definite for σ² > 0.

theorem posDef_serCov [Finite n] {σ2 : ℝ≥0} (hσ : σ2 ≠ 0) (σ02 : ℝ≥0)
    (x : EuclideanSpace ℝ n) : (serCov σ2 σ02 x).PosDef

Uses 1 · Used by 2

Statement usesCovariance of the single-effect regression model

Used byThe effect posterior of the single-effect regression · The marginal law of the phenotype given the causal variant

TheoremThe marginal law of the phenotype given the causal variant#✓fully proved

If y = x β + e with β ~ N(0, σ₀²) independent of e ~ N(0, σ² I), then y has density multivariateGaussianPDFReal 0 (serCov σ2 σ02 x).

theorem map_ser_eq_withDensity {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    [IsProbabilityMeasure P] {β : Ω → EuclideanSpace ℝ Unit} {e : Ω → EuclideanSpace ℝ n}
    (hβ : Measurable β) (he : Measurable e) (hind : IndepFun β e P) {σ2 σ02 : ℝ≥0}
    (hσ : σ2 ≠ 0) (hβl : P.map β = multivariateGaussian 0 ((σ02 : ℝ) • 1))
    (hel : P.map e = multivariateGaussian 0 ((σ2 : ℝ) • 1)) (x : EuclideanSpace ℝ n) :
    P.map (fun ω => toEuclideanLin (replicateCol Unit (ofLp x)) (β ω) + e ω) =
      volume.withDensity fun y =>
        ENNReal.ofReal (multivariateGaussianPDFReal 0 (serCov σ2 σ02 x) y)

Uses 5

Statement usesCovariance of the single-effect regression model · Multivariate Gaussian density function

Proof usesSingle-effect regression covariance is positive definite · The marginal of a linear-Gaussian model · The multivariate Gaussian density

TheoremThe regression Bayes factor is the Wakefield ABF#✓fully proved

The regression Bayes factor is the Wakefield ABF (Wang et al. 2020): the density of y when variant x carries an N(0, σ₀²) effect, divided by its density with no effect, is the ABF of the summary statistics olsEffect x y and olsVar σ2 x.

theorem multivariateGaussianPDFReal_serCov_div {σ2 : ℝ≥0} (hσ : σ2 ≠ 0) (σ02 : ℝ≥0)
    {x : EuclideanSpace ℝ n} (hx : x ≠ 0) (y : EuclideanSpace ℝ n) :
    multivariateGaussianPDFReal 0 (serCov σ2 σ02 x) y /
        multivariateGaussianPDFReal 0 (serCov σ2 0 x) y =
      wakefieldABF (olsVar σ2 x) σ02 (olsEffect x y)

Uses 6 · Used by 1

Statement usesMarginal least-squares effect estimate · Sampling variance of the least-squares effect estimate · Covariance of the single-effect regression model · Wakefield's approximate Bayes factor · Multivariate Gaussian density function

Proof usesWakefield's closed form

Used bySingle-effect likelihood-ratio identity

StructurePrior weights over the causal variant#✓fully proved

A finite probability distribution used as the prior over the single causal variant.

structure PriorWeights (ι : Type*) [Fintype ι] where
  /-- The prior probability of each variant. -/
  weight : ι → ℝ
  weight_nonneg : ∀ j, 0 ≤ weight j
  sum_weight : ∑ j, weight j = 1

Used by 7

Used byPositivity of the prior-weighted marginal likelihood · A normalized prior gives some variant positive weight · Posterior inclusion probability · Nonnegativity of posterior inclusion probabilities · Posterior inclusion probabilities of the single-effect regression · Positivity of the single-effect regression evidence · Posterior inclusion probabilities sum to one

TheoremA normalized prior gives some variant positive weight#✓fully proved

A normalized non-negative finite prior assigns positive weight to some variant.

theorem exists_weight_pos {ι : Type*} [Fintype ι] (w : PriorWeights ι) :
    ∃ j, 0 < w j

Uses 1 · Used by 1

Statement usesPrior weights over the causal variant

Used byPositivity of the prior-weighted marginal likelihood

TheoremPositivity of the prior-weighted marginal likelihood#✓fully proved

Strictly positive evidence has a strictly positive prior-weighted marginal likelihood.

theorem evidence_pos {ι : Type*} [Fintype ι] (w : PriorWeights ι) {BF : ι → ℝ}
    (hBF : ∀ j, 0 < BF j) : 0 < ∑ j, w j * BF j

Uses 2 · Used by 3

Statement usesPrior weights over the causal variant

Proof usesA normalized prior gives some variant positive weight

Used byNonnegativity of posterior inclusion probabilities · Positivity of the single-effect regression evidence · Posterior inclusion probabilities sum to one

DefinitionNormalized weighted evidence#✓fully proved

Algebraic normalization of arbitrary weights times evidence. This is useful even outside the probability domain; it takes Lean's value 0 when the denominator vanishes.

noncomputable def normalizedWeightedEvidence {ι : Type*} [Fintype ι]
    (w BF : ι → ℝ) (j : ι) : ℝ :=
  w j * BF j / ∑ k, w k * BF k

Used by 2

Used byPosterior inclusion probability · Single-effect likelihood-ratio identity

DefinitionPosterior inclusion probability#✓fully proved

Posterior inclusion probability from a normalized non-negative prior and variant evidence. When every evidence value is positive, PriorWeights.evidence_pos makes the denominator strictly positive, and pip_nonneg and sum_pip prove that these values form a probability distribution.

noncomputable def pip {ι : Type*} [Fintype ι] (w : PriorWeights ι)
    (BF : ι → ℝ) (j : ι) : ℝ :=
  normalizedWeightedEvidence w.weight BF j

Uses 2 · Used by 3

Statement usesPrior weights over the causal variant · Normalized weighted evidence

Used byNonnegativity of posterior inclusion probabilities · Posterior inclusion probabilities of the single-effect regression · Posterior inclusion probabilities sum to one

TheoremNonnegativity of posterior inclusion probabilities#✓fully proved

Posterior inclusion probabilities are non-negative when every evidence value is positive.

theorem pip_nonneg {ι : Type*} [Fintype ι] (w : PriorWeights ι) {BF : ι → ℝ}
    (hBF : ∀ j, 0 < BF j) (j : ι) : 0 ≤ pip w BF j

Uses 3

Statement usesPrior weights over the causal variant · Posterior inclusion probability

Proof usesPositivity of the prior-weighted marginal likelihood

TheoremPosterior inclusion probabilities sum to one#✓fully proved

Posterior inclusion probabilities normalize to one when every evidence value is positive.

theorem sum_pip {ι : Type*} [Fintype ι] (w : PriorWeights ι) {BF : ι → ℝ}
    (hBF : ∀ j, 0 < BF j) : ∑ j, pip w BF j = 1

Uses 3

Statement usesPrior weights over the causal variant · Posterior inclusion probability

Proof usesPositivity of the prior-weighted marginal likelihood

TheoremSingle-effect likelihood-ratio identity#✓fully proved

The unconditional algebraic single-effect likelihood-ratio identity for arbitrary real weights. Its right side is accurately named algebraic normalization, not a posterior probability.

theorem serLikelihoodRatio_eq_normalizedWeightedEvidence {ι : Type*} [Fintype ι]
    (w : ι → ℝ) {σ2 : ℝ≥0} (hσ : σ2 ≠ 0)
    (σ02 : ℝ≥0) (X : ι → EuclideanSpace ℝ n) (hX : ∀ k, X k ≠ 0) (y : EuclideanSpace ℝ n)
    (j : ι) :
    w j * multivariateGaussianPDFReal 0 (serCov σ2 σ02 (X j)) y /
        ∑ k, w k * multivariateGaussianPDFReal 0 (serCov σ2 σ02 (X k)) y =
      normalizedWeightedEvidence w
        (fun k => wakefieldABF (olsVar σ2 (X k)) σ02 (olsEffect (X k) y)) j

Uses 7 · Used by 1

Statement usesNormalized weighted evidence · Marginal least-squares effect estimate · Sampling variance of the least-squares effect estimate · Covariance of the single-effect regression model · Wakefield's approximate Bayes factor · Multivariate Gaussian density function

Proof usesThe regression Bayes factor is the Wakefield ABF

Used byPosterior inclusion probabilities of the single-effect regression

TheoremPositivity of the single-effect regression evidence#✓fully proved

The prior-weighted single-effect evidence is strictly positive on the regression domain.

theorem serPosterior_evidence_pos {ι : Type*} [Fintype ι] (w : PriorWeights ι)
    {σ2 : ℝ≥0} (hσ : σ2 ≠ 0) (σ02 : ℝ≥0) (X : ι → EuclideanSpace ℝ n)
    (hX : ∀ k, X k ≠ 0) (y : EuclideanSpace ℝ n) :
    0 < ∑ k, w k * wakefieldABF (olsVar σ2 (X k)) σ02 (olsEffect (X k) y)

Uses 6

Statement usesPrior weights over the causal variant · Marginal least-squares effect estimate · Sampling variance of the least-squares effect estimate · Wakefield's approximate Bayes factor

Proof usesPositivity of the prior-weighted marginal likelihood · Positivity of Wakefield's approximate Bayes factor

TheoremPosterior inclusion probabilities of the single-effect regression#✓fully proved

Posterior inclusion probabilities of the single-effect regression (Wang et al. 2020): Bayes' rule for the causal variant with a normalized non-negative prior equals pip applied to the strictly positive Wakefield ABFs.

theorem serPosterior_eq_pip {ι : Type*} [Fintype ι] (w : PriorWeights ι)
    {σ2 : ℝ≥0} (hσ : σ2 ≠ 0) (σ02 : ℝ≥0) (X : ι → EuclideanSpace ℝ n)
    (hX : ∀ k, X k ≠ 0) (y : EuclideanSpace ℝ n) (j : ι) :
    w j * multivariateGaussianPDFReal 0 (serCov σ2 σ02 (X j)) y /
        ∑ k, w k * multivariateGaussianPDFReal 0 (serCov σ2 σ02 (X k)) y =
      pip w (fun k => wakefieldABF (olsVar σ2 (X k)) σ02 (olsEffect (X k) y)) j

Uses 8

Statement usesPrior weights over the causal variant · Marginal least-squares effect estimate · Sampling variance of the least-squares effect estimate · Posterior inclusion probability · Covariance of the single-effect regression model · Wakefield's approximate Bayes factor · Multivariate Gaussian density function

Proof usesSingle-effect likelihood-ratio identity

TheoremThe effect posterior of the single-effect regression#✓fully proved

The effect posterior of the single-effect regression (Wang et al. 2020): given y = x β + e with β ~ N(0, σ₀²) independent of e ~ N(0, σ² I), for almost every y the effect is normal with mean σ₀² / (σ₀² + s²) · β̂ and variance σ₀² s² / (σ₀² + s²), where β̂ = olsEffect x y and s² = olsVar σ2 x.

theorem condDistrib_ser_effect {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    [IsProbabilityMeasure P] {β : Ω → EuclideanSpace ℝ Unit} {e : Ω → EuclideanSpace ℝ n}
    (hβ : Measurable β) (he : Measurable e) (hind : IndepFun β e P) {σ2 σ02 : ℝ≥0}
    (hσ : σ2 ≠ 0) (hβl : P.map β = multivariateGaussian 0 ((σ02 : ℝ) • 1))
    (hel : P.map e = multivariateGaussian 0 ((σ2 : ℝ) • 1)) {x : EuclideanSpace ℝ n}
    (hx : x ≠ 0) :
    ∀ᵐ y ∂P.map (fun ω => toEuclideanLin (replicateCol Unit (ofLp x)) (β ω) + e ω),
      condDistrib β (fun ω => toEuclideanLin (replicateCol Unit (ofLp x)) (β ω) + e ω) P y =
        multivariateGaussian
          (EuclideanSpace.single () ((σ02 : ℝ) / (σ02 + olsVar σ2 x) * olsEffect x y))
          (((σ02 : ℝ) * olsVar σ2 x / (σ02 + olsVar σ2 x)) • 1)

Uses 5

Statement usesMarginal least-squares effect estimate · Sampling variance of the least-squares effect estimate

Proof usesSingle-effect regression covariance is positive definite · Covariance of the single-effect regression model · Bayes' theorem for a linear-Gaussian observation

Colocalization

InductiveThe five colocalization hypotheses#✓fully proved

The five coloc hypotheses: no association (h0), trait 1 only (h1), trait 2 only (h2), two distinct causal variants (h3), one shared causal variant (h4).

inductive ColocHypothesis
  | h0 | h1 | h2 | h3 | h4
  deriving DecidableEq

Used by 16

Used byNormalized categorical colocalization prior · Nonnegativity of categorical configuration priors · Closed-form scores for the categorical colocalization prior · Posterior identity for the categorical colocalization prior · Closed-form colocalization hypothesis scores · Nonnegativity of closed-form colocalization scores · Positivity of colocalization evidence · Colocalization hypothesis of a causal configuration · Colocalization normalization identity · Nonnegativity of colocalization posteriors · Categorical colocalization priors sum to one · Categorical-prior hypothesis scores equal their closed forms · Colocalization posteriors sum to one · The coloc closed forms · Unnormalized colocalization configuration weight · Nonnegativity of colocalization configuration weights

DefinitionColocalization hypothesis of a causal configuration#✓fully proved

The hypothesis of a configuration (causal variant of trait 1, causal variant of trait 2), none meaning no causal variant.

def colocHypothesis : Option ι × Option ι → ColocHypothesis
  | (none, none) => .h0
  | (some _, none) => .h1
  | (none, some _) => .h2
  | (some j, some k) => if j = k then .h4 else .h3

Uses 1 · Used by 10

Statement usesThe five colocalization hypotheses

Used byNormalized categorical colocalization prior · Nonnegativity of categorical configuration priors · Posterior identity for the categorical colocalization prior · Nonnegativity of closed-form colocalization scores · Colocalization normalization identity · Categorical colocalization priors sum to one · Categorical-prior hypothesis scores equal their closed forms · The coloc closed forms · Unnormalized colocalization configuration weight · Nonnegativity of colocalization configuration weights

StructureColocalization prior parameters#✓fully proved

Non-negative coloc configuration-weight parameters (Giambartolomei et al. 2014): p1, p2, p12 for a variant causal for trait 1 only, trait 2 only, and both. The cited hypothesis weights use null weight 1. The bound also supports a separate normalized categorical-prior model.

structure ColocPrior (ι : Type*) [Fintype ι] where
  /-- Weight of a configuration in `h1`. -/
  p1 : ℝ
  /-- Weight of a configuration in `h2`. -/
  p2 : ℝ
  /-- Weight of a configuration in `h4`. -/
  p12 : ℝ
  p1_nonneg : 0 ≤ p1
  p2_nonneg : 0 ≤ p2
  p12_nonneg : 0 ≤ p12
  /-- The optional categorical priors leave non-negative mass for the null configuration. -/
  sum_le_one : (Fintype.card ι : ℝ) * p1 + Fintype.card ι * p2 +
    Fintype.card ι * (Fintype.card ι - 1) * (p1 * p2) + Fintype.card ι * p12 ≤ 1

Used by 16

Used byNormalized categorical colocalization prior · Nonnegativity of categorical configuration priors · Closed-form scores for the categorical colocalization prior · Posterior identity for the categorical colocalization prior · Closed-form colocalization hypothesis scores · Nonnegativity of closed-form colocalization scores · Positivity of colocalization evidence · Colocalization normalization identity · Nonnegativity of colocalization posteriors · Null mass of the categorical colocalization prior · Categorical colocalization priors sum to one · Categorical-prior hypothesis scores equal their closed forms · Colocalization posteriors sum to one · The coloc closed forms · Unnormalized colocalization configuration weight · Nonnegativity of colocalization configuration weights

DefinitionNull mass of the categorical colocalization prior#✓fully proved

The remaining null mass in the optional normalized categorical-prior model.

def p0 : ℝ :=
  1 - ((Fintype.card ι : ℝ) * P.p1 + Fintype.card ι * P.p2 +
    Fintype.card ι * (Fintype.card ι - 1) * (P.p1 * P.p2) + Fintype.card ι * P.p12)

Uses 1 · Used by 5

Statement usesColocalization prior parameters

Used byNormalized categorical colocalization prior · Nonnegativity of categorical configuration priors · Closed-form scores for the categorical colocalization prior · Categorical colocalization priors sum to one · Categorical-prior hypothesis scores equal their closed forms

DefinitionNormalized categorical colocalization prior#✓fully proved

A normalized categorical prior, distinct from the cited coloc relative weights.

def categoricalPrior (S : Option ι × Option ι) : ℝ :=
  match colocHypothesis S with
  | .h0 => P.p0
  | .h1 => P.p1
  | .h2 => P.p2
  | .h3 => P.p1 * P.p2
  | .h4 => P.p12

Uses 4 · Used by 4

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Null mass of the categorical colocalization prior · Colocalization hypothesis of a causal configuration

Used byNonnegativity of categorical configuration priors · Posterior identity for the categorical colocalization prior · Categorical colocalization priors sum to one · Categorical-prior hypothesis scores equal their closed forms

DefinitionUnnormalized colocalization configuration weight#✓fully proved

The cited coloc unnormalized configuration weight, whose H0 weight is 1.

def weight (S : Option ι × Option ι) : ℝ :=
  match colocHypothesis S with
  | .h0 => 1
  | .h1 => P.p1
  | .h2 => P.p2
  | .h3 => P.p1 * P.p2
  | .h4 => P.p12

Uses 3 · Used by 4

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Colocalization hypothesis of a causal configuration

Used byNonnegativity of closed-form colocalization scores · Colocalization normalization identity · The coloc closed forms · Nonnegativity of colocalization configuration weights

TheoremNonnegativity of categorical configuration priors#✓fully proved

Categorical configuration priors are non-negative.

theorem categoricalPrior_nonneg (S : Option ι × Option ι) : 0 ≤ P.categoricalPrior S

Uses 5

Statement usesColocalization prior parameters · Normalized categorical colocalization prior

Proof usesThe five colocalization hypotheses · Null mass of the categorical colocalization prior · Colocalization hypothesis of a causal configuration

TheoremNonnegativity of colocalization configuration weights#✓fully proved

Cited coloc configuration weights are non-negative.

theorem weight_nonneg (S : Option ι × Option ι) : 0 ≤ P.weight S

Uses 4 · Used by 1

Statement usesColocalization prior parameters · Unnormalized colocalization configuration weight

Proof usesThe five colocalization hypotheses · Colocalization hypothesis of a causal configuration

Used byNonnegativity of closed-form colocalization scores

DefinitionBayes factor of a colocalization configuration#✓fully proved

The Bayes factor of a configuration against the null: the product of the two traits' Bayes factors, 1 for a trait without a causal variant (the two studies are independent).

def colocBF (bf1 bf2 : ι → ℝ) (S : Option ι × Option ι) : ℝ :=
  S.1.elim 1 bf1 * S.2.elim 1 bf2

Used by 7

Used byNonnegativity of configuration Bayes factors · Posterior identity for the categorical colocalization prior · Nonnegativity of closed-form colocalization scores · Colocalization normalization identity · Categorical colocalization priors sum to one · Categorical-prior hypothesis scores equal their closed forms · The coloc closed forms

TheoremNonnegativity of configuration Bayes factors#✓fully proved

A configuration Bayes factor is non-negative when both traits' Bayes factors are.

theorem colocBF_nonneg (bf1 bf2 : ι → ℝ) (hbf1 : ∀ j, 0 ≤ bf1 j)
    (hbf2 : ∀ j, 0 ≤ bf2 j) (S : Option ι × Option ι) : 0 ≤ colocBF bf1 bf2 S

Uses 1 · Used by 1

Statement usesBayes factor of a colocalization configuration

Used byNonnegativity of closed-form colocalization scores

DefinitionClosed-form colocalization hypothesis scores#✓fully proved

The cited coloc closed-form algebraic scores. H0 has score 1; H1--H4 retain the per-configuration coefficients of Giambartolomei et al. (2014). They are unnormalized hypothesis weights, and hence have a probability interpretation, when the Bayes factors are non-negative.

def colocClosedForm (P : ColocPrior ι) (bf1 bf2 : ι → ℝ) : ColocHypothesis → ℝ
  | .h0 => 1
  | .h1 => P.p1 * ∑ j, bf1 j
  | .h2 => P.p2 * ∑ k, bf2 k
  | .h3 => P.p1 * P.p2 * ((∑ j, bf1 j) * (∑ k, bf2 k) - ∑ j, bf1 j * bf2 j)
  | .h4 => P.p12 * ∑ j, bf1 j * bf2 j

Uses 2 · Used by 6

Statement usesThe five colocalization hypotheses · Colocalization prior parameters

Used byNonnegativity of closed-form colocalization scores · Positivity of colocalization evidence · Colocalization normalization identity · Nonnegativity of colocalization posteriors · Colocalization posteriors sum to one · The coloc closed forms

DefinitionClosed-form scores for the categorical colocalization prior#✓fully proved

Closed forms for the optional normalized categorical-prior model. This differs from the cited coloc formula only in using its remaining null mass rather than the cited H0 weight 1.

def colocCategoricalClosedForm (P : ColocPrior ι) (bf1 bf2 : ι → ℝ) :
    ColocHypothesis → ℝ
  | .h0 => P.p0
  | .h1 => P.p1 * ∑ j, bf1 j
  | .h2 => P.p2 * ∑ k, bf2 k
  | .h3 => P.p1 * P.p2 * ((∑ j, bf1 j) * (∑ k, bf2 k) - ∑ j, bf1 j * bf2 j)
  | .h4 => P.p12 * ∑ j, bf1 j * bf2 j

Uses 3 · Used by 3

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Null mass of the categorical colocalization prior

Used byPosterior identity for the categorical colocalization prior · Categorical colocalization priors sum to one · Categorical-prior hypothesis scores equal their closed forms

TheoremThe coloc closed forms#✓fully proved

The coloc closed forms (Giambartolomei et al. 2014): the sum of unnormalized configuration weight times Bayes factor over each hypothesis equals its closed form.

theorem sum_colocWeight_mul_colocBF (P : ColocPrior ι) (bf1 bf2 : ι → ℝ)
    (h : ColocHypothesis) :
    ∑ S ∈ Finset.univ.filter (fun S => colocHypothesis S = h), P.weight S * colocBF bf1 bf2 S =
      colocClosedForm P bf1 bf2 h

Uses 6 · Used by 2

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Unnormalized colocalization configuration weight · Bayes factor of a colocalization configuration · Closed-form colocalization hypothesis scores · Colocalization hypothesis of a causal configuration

Used byNonnegativity of closed-form colocalization scores · Colocalization normalization identity

TheoremNonnegativity of closed-form colocalization scores#✓fully proved

Cited coloc closed-form scores are non-negative on the Bayes-factor domain.

theorem colocClosedForm_nonneg (P : ColocPrior ι) (bf1 bf2 : ι → ℝ)
    (hbf1 : ∀ j, 0 ≤ bf1 j) (hbf2 : ∀ j, 0 ≤ bf2 j) (h : ColocHypothesis) :
    0 ≤ colocClosedForm P bf1 bf2 h

Uses 9 · Used by 2

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Closed-form colocalization hypothesis scores

Proof usesUnnormalized colocalization configuration weight · Nonnegativity of colocalization configuration weights · Bayes factor of a colocalization configuration · Nonnegativity of configuration Bayes factors · Colocalization hypothesis of a causal configuration · The coloc closed forms

Used byPositivity of colocalization evidence · Nonnegativity of colocalization posteriors

TheoremPositivity of colocalization evidence#✓fully proved

Cited coloc evidence is strictly positive for non-negative Bayes factors because H0 has unnormalized weight 1.

theorem colocEvidence_pos (P : ColocPrior ι) (bf1 bf2 : ι → ℝ)
    (hbf1 : ∀ j, 0 ≤ bf1 j) (hbf2 : ∀ j, 0 ≤ bf2 j) :
    0 < ∑ h, colocClosedForm P bf1 bf2 h

Uses 4 · Used by 2

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Closed-form colocalization hypothesis scores

Proof usesNonnegativity of closed-form colocalization scores

Used byNonnegativity of colocalization posteriors · Colocalization posteriors sum to one

TheoremCategorical-prior hypothesis scores equal their closed forms#✓fully proved

The corresponding closed forms for the optional normalized categorical-prior model.

theorem sum_categoricalPrior_mul_colocBF (P : ColocPrior ι) (bf1 bf2 : ι → ℝ)
    (h : ColocHypothesis) :
    ∑ S ∈ Finset.univ.filter (fun S => colocHypothesis S = h),
        P.categoricalPrior S * colocBF bf1 bf2 S = colocCategoricalClosedForm P bf1 bf2 h

Uses 7 · Used by 2

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Normalized categorical colocalization prior · Bayes factor of a colocalization configuration · Closed-form scores for the categorical colocalization prior · Colocalization hypothesis of a causal configuration

Proof usesNull mass of the categorical colocalization prior

Used byPosterior identity for the categorical colocalization prior · Categorical colocalization priors sum to one

TheoremCategorical colocalization priors sum to one#✓fully proved

The optional categorical configuration priors sum to one.

theorem ColocPrior.sum_categoricalPrior (P : ColocPrior ι) :
    ∑ S, P.categoricalPrior S = 1

Uses 8

Statement usesColocalization prior parameters · Normalized categorical colocalization prior

Proof usesThe five colocalization hypotheses · Null mass of the categorical colocalization prior · Bayes factor of a colocalization configuration · Closed-form scores for the categorical colocalization prior · Colocalization hypothesis of a causal configuration · Categorical-prior hypothesis scores equal their closed forms

TheoremColocalization normalization identity#✓fully proved

The unconditional algebraic coloc normalization identity: each hypothesis's configuration score divided by the total score equals its closed-form score divided by the closed-form total. For arbitrary real bf1 and bf2 these ratios need not be probabilities. See colocPosterior_nonneg and sum_colocPosterior_eq_one for the probability-domain results.

theorem colocPosterior_eq (P : ColocPrior ι) (bf1 bf2 : ι → ℝ) (h : ColocHypothesis) :
    (∑ S ∈ Finset.univ.filter (fun S => colocHypothesis S = h), P.weight S * colocBF bf1 bf2 S) /
        ∑ S, P.weight S * colocBF bf1 bf2 S =
      colocClosedForm P bf1 bf2 h / ∑ h', colocClosedForm P bf1 bf2 h'

Uses 7

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Unnormalized colocalization configuration weight · Bayes factor of a colocalization configuration · Closed-form colocalization hypothesis scores · Colocalization hypothesis of a causal configuration

Proof usesThe coloc closed forms

TheoremNonnegativity of colocalization posteriors#✓fully proved

Normalized cited coloc hypothesis weights are non-negative for non-negative Bayes factors.

theorem colocPosterior_nonneg (P : ColocPrior ι) (bf1 bf2 : ι → ℝ)
    (hbf1 : ∀ j, 0 ≤ bf1 j) (hbf2 : ∀ j, 0 ≤ bf2 j) (h : ColocHypothesis) :
    0 ≤ colocClosedForm P bf1 bf2 h / ∑ h', colocClosedForm P bf1 bf2 h'

Uses 5

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Closed-form colocalization hypothesis scores

Proof usesNonnegativity of closed-form colocalization scores · Positivity of colocalization evidence

TheoremColocalization posteriors sum to one#✓fully proved

Normalized cited coloc hypothesis weights sum to one for non-negative Bayes factors.

theorem sum_colocPosterior_eq_one (P : ColocPrior ι) (bf1 bf2 : ι → ℝ)
    (hbf1 : ∀ j, 0 ≤ bf1 j) (hbf2 : ∀ j, 0 ≤ bf2 j) :
    ∑ h, colocClosedForm P bf1 bf2 h / ∑ h', colocClosedForm P bf1 bf2 h' = 1

Uses 4

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Closed-form colocalization hypothesis scores

Proof usesPositivity of colocalization evidence

TheoremPosterior identity for the categorical colocalization prior#✓fully proved

The normalized posterior identity for the separate categorical-prior model.

theorem colocCategoricalPosterior_eq (P : ColocPrior ι) (bf1 bf2 : ι → ℝ)
    (h : ColocHypothesis) :
    (∑ S ∈ Finset.univ.filter (fun S => colocHypothesis S = h),
        P.categoricalPrior S * colocBF bf1 bf2 S) /
        ∑ S, P.categoricalPrior S * colocBF bf1 bf2 S =
      colocCategoricalClosedForm P bf1 bf2 h /
        ∑ h', colocCategoricalClosedForm P bf1 bf2 h'

Uses 7

Statement usesThe five colocalization hypotheses · Colocalization prior parameters · Normalized categorical colocalization prior · Bayes factor of a colocalization configuration · Closed-form scores for the categorical colocalization prior · Colocalization hypothesis of a causal configuration

Proof usesCategorical-prior hypothesis scores equal their closed forms

Credible sets

DefinitionCredible set of variants#✓fully proved

A ρ-credible set: its total posterior inclusion probability is at least ρ.

def IsCredibleSet (α : ι → ℝ) (ρ : ℝ) (S : Finset ι) : Prop := ρ ≤ ∑ j ∈ S, α j

Used by 2

Used byA minimum-size credible set exists and is a sorted prefix · The shortest credible prefix has minimum size

DefinitionPrefix of variants in a given order#✓fully proved

The first k variants in the order σ.

def sortedPrefix (σ : Fin (Fintype.card ι) ≃ ι) (k : ℕ) : Finset ι :=
  (Finset.univ.filter fun i : Fin (Fintype.card ι) => i.val < k).map σ.toEmbedding

Used by 4

Used byCardinality of a sorted prefix · A minimum-size credible set exists and is a sorted prefix · The shortest credible prefix has minimum size · Sorted prefix carries the most posterior mass

TheoremCardinality of a sorted prefix#✓fully proved

A prefix of length k ≤ card ι has k elements.

theorem card_sortedPrefix (σ : Fin (Fintype.card ι) ≃ ι) {k : ℕ} (hk : k ≤ Fintype.card ι) :
    (sortedPrefix σ k).card = k

Uses 1 · Used by 1

Statement usesPrefix of variants in a given order

Used byA minimum-size credible set exists and is a sorted prefix

TheoremSorted prefix carries the most posterior mass#✓fully proved

The k largest values carry the most mass: if σ sorts α in decreasing order, no set of S.card variants has more mass than the prefix of that length.

theorem sum_le_sum_sortedPrefix (α : ι → ℝ) {σ : Fin (Fintype.card ι) ≃ ι}
    (hσ : Antitone (α ∘ σ)) (S : Finset ι) :
    ∑ j ∈ S, α j ≤ ∑ j ∈ sortedPrefix σ S.card, α j

Uses 1 · Used by 1

Statement usesPrefix of variants in a given order

Used byThe shortest credible prefix has minimum size

TheoremThe shortest credible prefix has minimum size#✓fully proved

The shortest credible prefix has minimum size (Maller et al. 2012; Wang et al. 2020): if σ sorts α in decreasing order and no prefix shorter than k is ρ-credible, every ρ-credible set has at least k elements.

theorem le_card_of_isCredibleSet (α : ι → ℝ) {σ : Fin (Fintype.card ι) ≃ ι}
    (hσ : Antitone (α ∘ σ)) {ρ : ℝ} {k : ℕ}
    (hk : ∀ m < k, ¬IsCredibleSet α ρ (sortedPrefix σ m)) {S : Finset ι}
    (hS : IsCredibleSet α ρ S) : k ≤ S.card

Uses 3 · Used by 1

Statement usesCredible set of variants · Prefix of variants in a given order

Proof usesSorted prefix carries the most posterior mass

Used byA minimum-size credible set exists and is a sorted prefix

TheoremA minimum-size credible set exists and is a sorted prefix#✓fully proved

If the total mass is at least ρ, some prefix of length k is ρ-credible, has k elements, and every ρ-credible set has at least k elements.

theorem exists_minimal_credible_prefix (α : ι → ℝ) {σ : Fin (Fintype.card ι) ≃ ι}
    (hσ : Antitone (α ∘ σ)) {ρ : ℝ} (hρ : ρ ≤ ∑ j, α j) :
    ∃ k, IsCredibleSet α ρ (sortedPrefix σ k) ∧ (sortedPrefix σ k).card = k ∧
      ∀ S, IsCredibleSet α ρ S → k ≤ S.card

Uses 4

Statement usesCredible set of variants · Prefix of variants in a given order

Proof usesCardinality of a sorted prefix · The shortest credible prefix has minimum size

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.