Meta-analysis

DefinitionFisher's combined statistic#✓fully proved

Fisher's combined statistic -2 ∑ log pᵢ of k p-values.

noncomputable def fisherStatistic (p : Fin k → ℝ) : ℝ := -2 * ∑ i, Real.log (p i)

Used by 1

Used byFisher's method for combining p-values

TheoremMinus twice the log of a uniform variable is chi-square#✓fully proved

-2 log U has the exponential law of rate 1/2, i.e. chi-square with two degrees of freedom, when U is uniform on [0, 1].

theorem hasLaw_neg_two_mul_log_uniform :
    HasLaw (fun u : ℝ => -2 * Real.log u) (gammaMeasure 1 (1 / 2))
      (volume.restrict (Icc (0 : ℝ) 1))

Used by 1

Used byFisher's method for combining p-values

TheoremFisher's method for combining p-values#✓fully proved

Fisher (1932), §21.1: for k ≥ 1 independent p-values, each uniform on [0, 1], Fisher's statistic -2 ∑ log pᵢ is chi-square with 2k degrees of freedom.

theorem hasLaw_fisherStatistic (hk : 0 < k) {μ : Measure Ω} [IsProbabilityMeasure μ]
    {p : Fin k → Ω → ℝ} (hlaw : ∀ i, HasLaw (p i) (volume.restrict (Set.Icc (0 : ℝ) 1)) μ)
    (hind : iIndepFun p μ) :
    HasLaw (fun ω => fisherStatistic fun i => p i ω) (chiSquareMeasure (2 * k)) μ

Uses 5

Statement usesFisher's combined statistic · Chi-square distribution

Proof usesMinus twice the log of a uniform variable is chi-square · Moment generating function determines the gamma law · Moment generating function of the gamma distribution

DefinitionStouffer's weighted z statistic#✓fully proved

Stouffer's weighted z statistic ∑ wᵢ zᵢ / √(∑ wᵢ²) of the study z-scores zᵢ.

noncomputable def stoufferStatistic (w z : Fin k → ℝ) : ℝ :=
  (∑ i, w i * z i) / √(∑ i, w i ^ 2)

Used by 1

Used byStouffer's method

TheoremStouffer's method#✓fully proved

Stouffer's method (Stouffer et al. 1949; Liptak 1958): for independent standard normal z-scores and a nonzero weight vector, the weighted z statistic is standard normal.

theorem hasLaw_stoufferStatistic {μ : Measure Ω} [IsProbabilityMeasure μ] {w : Fin k → ℝ}
    (hw : w ≠ 0) {z : Fin k → Ω → ℝ} (hlaw : ∀ i, HasLaw (z i) (gaussianReal 0 1) μ)
    (hind : iIndepFun z μ) :
    HasLaw (fun ω => stoufferStatistic w fun i => z i ω) (gaussianReal 0 1) μ

Uses 1

Statement usesStouffer's weighted z statistic

DefinitionInverse-variance weights#✓fully proved

The inverse-variance (fixed-effect) weights vᵢ⁻¹ / ∑ⱼ vⱼ⁻¹ for study variances v.

noncomputable def inverseVarianceWeights (v : Fin k → ℝ) (i : Fin k) : ℝ :=
  (v i)⁻¹ / ∑ j, (v j)⁻¹

Used by 6

Used byCochran's heterogeneity statistic Q · Cochran's Q as a squared projection norm · Optimality of inverse-variance weights · Inverse-variance weights sum to one · Variance of the inverse-variance-weighted average · Cochran's minimum-variance theorem for weighted averages

TheoremInverse-variance weights sum to one#✓fully proved

The inverse-variance weights sum to one.

theorem sum_inverseVarianceWeights {v : Fin k → ℝ} (hv : ∀ i, 0 < v i) (hk : 0 < k) :
    ∑ i, inverseVarianceWeights v i = 1

Uses 1 · Used by 2

Statement usesInverse-variance weights

Used byCochran's Q as a squared projection norm · Optimality of inverse-variance weights

TheoremVariance of the inverse-variance-weighted average#✓fully proved

The variance ∑ wᵢ² vᵢ of the inverse-variance-weighted average is (∑ vᵢ⁻¹)⁻¹.

theorem sum_sq_mul_inverseVarianceWeights {v : Fin k → ℝ} (hv : ∀ i, 0 < v i) (hk : 0 < k) :
    ∑ i, inverseVarianceWeights v i ^ 2 * v i = (∑ j, (v j)⁻¹)⁻¹

Uses 1 · Used by 1

Statement usesInverse-variance weights

Used byCochran's minimum-variance theorem for weighted averages

TheoremOptimality of inverse-variance weights#✓fully proved

Optimality of inverse-variance weighting: for positive variances v and weights c summing to one, ∑ cᵢ² vᵢ ≥ (∑ vᵢ⁻¹)⁻¹. The gap is ∑ vᵢ (cᵢ - wᵢ)² for the inverse-variance weights w.

theorem inv_sum_inv_le_sum_sq_mul {v : Fin k → ℝ} (hv : ∀ i, 0 < v i) {c : Fin k → ℝ}
    (hc : ∑ i, c i = 1) :
    (∑ j, (v j)⁻¹)⁻¹ ≤ ∑ i, c i ^ 2 * v i

Uses 2 · Used by 1

Proof usesInverse-variance weights · Inverse-variance weights sum to one

Used byCochran's minimum-variance theorem for weighted averages

TheoremCochran's minimum-variance theorem for weighted averages#✓fully proved

Cochran (1954): for pairwise independent square-integrable estimates X i with positive variances, the inverse-variance-weighted average has variance (∑ Var[Xᵢ]⁻¹)⁻¹, the smallest variance among all weighted averages ∑ cᵢ Xᵢ with ∑ cᵢ = 1.

theorem variance_inverseVariance_le {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : Fin k → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ)
    (hind : Pairwise fun i j => X i ⟂ᵢ[μ] X j) (hv : ∀ i, 0 < Var[X i; μ])
    {c : Fin k → ℝ} (hc : ∑ i, c i = 1) :
    Var[fun ω => ∑ i, inverseVarianceWeights (fun j => Var[X j; μ]) i * X i ω; μ] =
        (∑ j, (Var[X j; μ])⁻¹)⁻¹ ∧
      (∑ j, (Var[X j; μ])⁻¹)⁻¹ ≤ Var[fun ω => ∑ i, c i * X i ω; μ]

Uses 3

Statement usesInverse-variance weights

Proof usesOptimality of inverse-variance weights · Variance of the inverse-variance-weighted average

DefinitionCochran's heterogeneity statistic Q#✓fully proved

Cochran's heterogeneity statistic Q = ∑ᵢ vᵢ⁻¹ (Xᵢ - ∑ⱼ wⱼ Xⱼ)² of the estimates X with variances v, where w = inverseVarianceWeights v.

noncomputable def cochranQ (v X : Fin k → ℝ) : ℝ :=
  ∑ i, (v i)⁻¹ * (X i - ∑ j, inverseVarianceWeights v j * X j) ^ 2

Uses 1 · Used by 2

Statement usesInverse-variance weights

Used byCochran's Q as a squared projection norm · Cochran (1954)

TheoremCochran's Q as a squared projection norm#✓fully proved

Algebraic core of Cochran's theorem for Q: if Xᵢ = θ + √vᵢ zᵢ with vᵢ > 0, then Q is the squared distance from z to the line spanned by a = (vᵢ^{-1/2})ᵢ, i.e. the squared norm of the projection of z onto the orthogonal complement of that line.

theorem cochranQ_eq_norm_sq {v : Fin k → ℝ} (hv : ∀ i, 0 < v i) (θ : ℝ)
    (z : EuclideanSpace ℝ (Fin k)) :
    cochranQ v (fun i => θ + √(v i) * z i) =
      ‖(Submodule.span ℝ {WithLp.toLp 2 fun i => (√(v i))⁻¹})ᗮ.starProjection z‖ ^ 2

Uses 3 · Used by 1

Statement usesCochran's heterogeneity statistic Q

Proof usesInverse-variance weights · Inverse-variance weights sum to one

Used byCochran (1954)

TheoremCochran (1954)#✓fully proved

For k ≥ 2 independent Gaussian estimates Xᵢ ~ N(θ, vᵢ) with positive known variances, Cochran's Q has the chi-square law with k - 1 degrees of freedom.

theorem hasLaw_cochranQ (hk : 2 ≤ k) {μ : Measure Ω} [IsProbabilityMeasure μ]
    {θ : ℝ} {v : Fin k → ℝ≥0} (hv : ∀ i, v i ≠ 0) {X : Fin k → Ω → ℝ}
    (hlaw : ∀ i, HasLaw (X i) (gaussianReal θ (v i)) μ) (hind : iIndepFun X μ) :
    HasLaw (fun ω => cochranQ (fun i => (v i : ℝ)) fun i => X i ω)
      (chiSquareMeasure (k - 1)) μ

Uses 4

Statement usesCochran's heterogeneity statistic Q · Chi-square distribution

Proof usesCochran's Q as a squared projection norm · Cochran's theorem

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.