Imputation of association summary statistics

11 fully proved

Summary Imputation

StructureSecond-moment model for summary-statistic imputation#✓fully proved

Square-integrable statistics z_t (untyped marker) and z_o (typed markers) with raw second moments 𝔼 z_o z_oᵀ = Σ_oo, 𝔼 z_t z_o = Σ_ot, 𝔼 z_t² = Σ_tt. These are the covariances of the ImpG null model when the statistics are centred.

MathlibExt.Biology.StatisticalGenetics.SummaryImputation.Model · 21 lines

structure Model (P : Measure Ω) (ι : Type*) where
  /-- The statistic of the untyped (target) marker. -/
  zt : Ω → ℝ
  /-- The statistics of the typed markers. -/
  zo : ι → Ω → ℝ
  /-- The target statistic is square integrable. -/
  memLp_zt : MemLp zt 2 P
  /-- The typed statistics are square integrable. -/
  memLp_zo : ∀ i, MemLp (zo i) 2 P
  /-- The LD (covariance) matrix `Σ_oo` among typed markers. -/
  sigmaOO : Matrix ι ι ℝ
  /-- The LD (covariance) vector `Σ_ot` between typed markers and the target. -/
  sigmaOT : ι → ℝ
  /-- The variance `Σ_tt` of the target statistic. -/
  sigmaTT : ℝ
  /-- `𝔼 z_o z_oᵀ = Σ_oo`. -/
  integral_zo_mul : ∀ i j, ∫ ω, zo i ω * zo j ω ∂P = sigmaOO i j
  /-- `𝔼 z_t z_o = Σ_ot`. -/
  integral_zt_mul : ∀ i, ∫ ω, zt ω * zo i ω ∂P = sigmaOT i
  /-- `𝔼 z_t² = Σ_tt`. -/
  integral_zt_sq : ∫ ω, zt ω ^ 2 ∂P = sigmaTT

Used by 10

Used byImputed summary statistic · Mean squared imputation error · Excess error of a linear imputation · ImpG is the best linear imputation · Mean squared error of imputation with ImpG weights · Cross moment of the imputed and untyped statistics · Second moment of the imputed statistic · Second moment of the statistic imputed with ImpG weights · Normalized imputed statistic · Symmetry of the typed-marker moment matrix

Model

DefinitionImputed summary statistic#✓fully proved

The imputed statistic ẑ = wᵀ z_o with weights w.

def imputed (w : ι → ℝ) (ω : Ω) : ℝ := ∑ i, w i * D.zo i ω

Uses 1 · Used by 8

Statement usesSecond-moment model for summary-statistic imputation

Used byMean squared imputation error · Excess error of a linear imputation · ImpG is the best linear imputation · Mean squared error of imputation with ImpG weights · Cross moment of the imputed and untyped statistics · Second moment of the imputed statistic · Second moment of the statistic imputed with ImpG weights · Normalized imputed statistic

TheoremSecond moment of the imputed statistic#✓fully proved

𝔼 ẑ² = wᵀ Σ_oo w.

theorem integral_imputed_sq (w : ι → ℝ) :
    ∫ ω, D.imputed w ω ^ 2 ∂P = w ⬝ᵥ (D.sigmaOO *ᵥ w)

Uses 2 · Used by 4

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Used byMean squared imputation error · ImpG is the best linear imputation · Second moment of the statistic imputed with ImpG weights · Normalized imputed statistic

TheoremCross moment of the imputed and untyped statistics#✓fully proved

𝔼 ẑ z_t = wᵀ Σ_ot.

theorem integral_imputed_mul (w : ι → ℝ) :
    ∫ ω, D.imputed w ω * D.zt ω ∂P = w ⬝ᵥ D.sigmaOT

Uses 2 · Used by 1

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Used byMean squared imputation error

TheoremMean squared imputation error#✓fully proved

The mean squared imputation error: 𝔼 (z_t - ẑ)² = Σ_tt - 2 wᵀ Σ_ot + wᵀ Σ_oo w.

theorem integral_error_sq (w : ι → ℝ) :
    ∫ ω, (D.zt ω - D.imputed w ω) ^ 2 ∂P =
      D.sigmaTT - 2 * (w ⬝ᵥ D.sigmaOT) + w ⬝ᵥ (D.sigmaOO *ᵥ w)

Uses 4 · Used by 2

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Proof usesCross moment of the imputed and untyped statistics · Second moment of the imputed statistic

Used byExcess error of a linear imputation · Mean squared error of imputation with ImpG weights

TheoremSecond moment of the statistic imputed with ImpG weights#✓fully proved

For the ImpG weights (Σ_oo w = Σ_ot, i.e. w = Σ_oo⁻¹ Σ_ot when Σ_oo is invertible) the imputed statistic has second moment wᵀ Σ_ot = Σ_to Σ_oo⁻¹ Σ_ot; for Σ_tt = 1 this is 1 - the linear-prediction residual variance, ImpG's r²_pred.

theorem integral_imputed_sq_of_normal {w : ι → ℝ} (hw : D.sigmaOO *ᵥ w = D.sigmaOT) :
    ∫ ω, D.imputed w ω ^ 2 ∂P = w ⬝ᵥ D.sigmaOT

Uses 3

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Proof usesSecond moment of the imputed statistic

TheoremMean squared error of imputation with ImpG weights#✓fully proved

For the ImpG weights (Σ_oo w = Σ_ot) the mean squared imputation error is Σ_tt - wᵀ Σ_ot = Σ_tt - Σ_to Σ_oo⁻¹ Σ_ot, the linear-prediction residual variance (the conditional variance only under the Gaussian ImpG model).

theorem integral_error_sq_of_normal {w : ι → ℝ} (hw : D.sigmaOO *ᵥ w = D.sigmaOT) :
    ∫ ω, (D.zt ω - D.imputed w ω) ^ 2 ∂P = D.sigmaTT - w ⬝ᵥ D.sigmaOT

Uses 3

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Proof usesMean squared imputation error

TheoremSymmetry of the typed-marker moment matrix#✓fully proved

The moment matrix Σ_oo is symmetric.

theorem sigmaOO_transpose : D.sigmaOOᵀ = D.sigmaOO

Uses 1 · Used by 1

Statement usesSecond-moment model for summary-statistic imputation

Used byExcess error of a linear imputation

TheoremExcess error of a linear imputation#✓fully proved

If Σ_oo w = Σ_ot, then for any weights w', 𝔼 (z_t - w'ᵀ z_o)² = 𝔼 (z_t - wᵀ z_o)² + (w' - w)ᵀ Σ_oo (w' - w).

theorem integral_error_sq_eq {w : ι → ℝ} (hw : D.sigmaOO *ᵥ w = D.sigmaOT) (w' : ι → ℝ) :
    ∫ ω, (D.zt ω - D.imputed w' ω) ^ 2 ∂P =
      ∫ ω, (D.zt ω - D.imputed w ω) ^ 2 ∂P + (w' - w) ⬝ᵥ (D.sigmaOO *ᵥ (w' - w))

Uses 4 · Used by 1

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Proof usesMean squared imputation error · Symmetry of the typed-marker moment matrix

Used byImpG is the best linear imputation

TheoremImpG is the best linear imputation#✓fully proved

The weights solving Σ_oo w = Σ_ot minimize the mean squared error 𝔼 (z_t - w'ᵀ z_o)² over all weights w'.

theorem integral_error_sq_le {w : ι → ℝ} (hw : D.sigmaOO *ᵥ w = D.sigmaOT) (w' : ι → ℝ) :
    ∫ ω, (D.zt ω - D.imputed w ω) ^ 2 ∂P ≤ ∫ ω, (D.zt ω - D.imputed w' ω) ^ 2 ∂P

Uses 4

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Proof usesExcess error of a linear imputation · Second moment of the imputed statistic

TheoremNormalized imputed statistic#✓fully proved

For any weights w with wᵀ Σ_oo w > 0 (for example the ridge weights solving (Σ_oo + λ I) w = Σ_ot), the statistic ẑ / √(wᵀ Σ_oo w) has second moment 1, so it has unit variance under the centred null.

theorem integral_normalized_sq (w : ι → ℝ) (hpos : 0 < w ⬝ᵥ (D.sigmaOO *ᵥ w)) :
    ∫ ω, (D.imputed w ω / Real.sqrt (w ⬝ᵥ (D.sigmaOO *ᵥ w))) ^ 2 ∂P = 1

Uses 3

Statement usesSecond-moment model for summary-statistic imputation · Imputed summary statistic

Proof usesSecond moment of the imputed statistic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.