Cross-population haplotype homozygosity

10 fully proved

Selection Scan

DefinitionExchangeable pair of statistics#✓fully proved

The pair of statistics (X, Y) is exchangeable under μ: the joint law is unchanged by swapping the two coordinates. This is an additional calibration assumption for a two-group haplotype test, stronger than the ordinary neutral null. Defined as IdentDistrib of the two orderings, so the measurability of the joint laws is part of the hypothesis rather than restored separately in each theorem.

def IsExchangeablePair (μ : Measure Ω) (X Y : Ω → ℝ) : Prop :=
  ProbabilityTheory.IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (Y ω, X ω)) μ μ

Used by 7

Used byExchangeability is preserved by a common measurable map · Difference of an exchangeable pair has a symmetric law · Two-sided rejection region splits into equal tails · Equal tails of the log ratio of an exchangeable pair · Equal tails of the ratio of an exchangeable pair · Equal tails of the difference of an exchangeable pair · Symmetry of the XP-EHH law under exchangeability

Is Exchangeable Pair

TheoremExchangeability is preserved by a common measurable map#✓fully proved

Applying the same measurable function to both statistics preserves exchangeability.

theorem map_comp (h : IsExchangeablePair μ X Y) (hX : Measurable X) (hY : Measurable Y)
    {f : ℝ → ℝ} (hf : Measurable f) :
    IsExchangeablePair μ (fun ω => f (X ω)) (fun ω => f (Y ω))

Uses 1 · Used by 1

Statement usesExchangeable pair of statistics

Used byEqual tails of the log ratio of an exchangeable pair

TheoremDifference of an exchangeable pair has a symmetric law#✓fully proved

The difference of an exchangeable pair has a symmetric law.

theorem map_sub_neg (h : IsExchangeablePair μ X Y) (hX : Measurable X) (hY : Measurable Y) :
    μ.map (fun ω => X ω - Y ω) = μ.map (fun ω => -(X ω - Y ω))

Uses 1 · Used by 1

Statement usesExchangeable pair of statistics

Used byEqual tails of the difference of an exchangeable pair

TheoremEqual tails of the difference of an exchangeable pair#✓fully proved

Equal tails: the upper tail of X - Y at t has the same probability as the lower tail at -t.

theorem measure_le_sub (h : IsExchangeablePair μ X Y) (hX : Measurable X) (hY : Measurable Y)
    (t : ℝ) : μ {ω | t ≤ X ω - Y ω} = μ {ω | X ω - Y ω ≤ -t}

Uses 2 · Used by 2

Statement usesExchangeable pair of statistics

Proof usesDifference of an exchangeable pair has a symmetric law

Used byTwo-sided rejection region splits into equal tails · Equal tails of the log ratio of an exchangeable pair

TheoremTwo-sided rejection region splits into equal tails#✓fully proved

A two-sided rejection region splits into two tails of equal probability.

theorem measure_abs_sub (h : IsExchangeablePair μ X Y) (hX : Measurable X) (hY : Measurable Y)
    {t : ℝ} (ht : 0 < t) :
    μ {ω | t ≤ |X ω - Y ω|} = 2 * μ {ω | t ≤ X ω - Y ω}

Uses 2

Statement usesExchangeable pair of statistics

Proof usesEqual tails of the difference of an exchangeable pair

TheoremEqual tails of the log ratio of an exchangeable pair#✓fully proved

For positive statistics, the log ratio — the XP-EHH form — has equal tails.

theorem measure_le_logRatio (h : IsExchangeablePair μ X Y) (hX : Measurable X)
    (hY : Measurable Y) (t : ℝ) :
    μ {ω | t ≤ log (X ω) - log (Y ω)} = μ {ω | log (X ω) - log (Y ω) ≤ -t}

Uses 3 · Used by 2

Statement usesExchangeable pair of statistics

Proof usesExchangeability is preserved by a common measurable map · Equal tails of the difference of an exchangeable pair

Used byEqual tails of the ratio of an exchangeable pair · Symmetry of the XP-EHH law under exchangeability

TheoremEqual tails of the ratio of an exchangeable pair#✓fully proved

The same statement for the ratio itself, the form used for relative EHH: the probability that the ratio exceeds c equals the probability that it falls below 1 / c.

theorem measure_le_ratio (h : IsExchangeablePair μ X Y) (hX : Measurable X) (hY : Measurable Y)
    (hXpos : ∀ ω, 0 < X ω) (hYpos : ∀ ω, 0 < Y ω) {c : ℝ} (hc : 0 < c) :
    μ {ω | c ≤ X ω / Y ω} = μ {ω | X ω / Y ω ≤ c⁻¹}

Uses 2

Statement usesExchangeable pair of statistics

Proof usesEqual tails of the log ratio of an exchangeable pair

Selection Scan

DefinitionCross-population extended haplotype homozygosity (XP-EHH)#✓fully proved

The cross-population extended haplotype homozygosity score (Sabeti et al. 2007): the log ratio of the integrated haplotype homozygosities of the same core region in two populations. Both arguments must be positive for the score to be meaningful. Outside that domain Real.log is totalized by Mathlib, not by the stated junk value: Real.log 0 = 0 and Real.log (-x) = Real.log x, so for example xpehh (-2) 1 = log 2.

noncomputable def xpehh (iA iB : ℝ) : ℝ := log iA - log iB

Used by 2

Used bySymmetry of the XP-EHH law under exchangeability · XP-EHH in star-genealogy sweep models

TheoremXP-EHH in star-genealogy sweep models#✓fully proved

XP-EHH computed from two star-genealogy sweep models with the same recombination rate is the log ratio of the two ages, with the opposite sign to ihs.

theorem xpehh_ihh {r T₁ T₂ : ℝ} (hr : 0 < r) (h₁ : 0 < T₁) (h₂ : 0 < T₂) :
    xpehh (ihh r T₁) (ihh r T₂) = log (T₂ / T₁)

Uses 3

Statement usesOne-sided integrated haplotype homozygosity · Cross-population extended haplotype homozygosity (XP-EHH)

Proof usesOne-sided iHH in the star-genealogy model

TheoremSymmetry of the XP-EHH law under exchangeability#✓fully proved

Under exchangeability, the XP-EHH score has a symmetric law: the two tails of the two-sided test carry the same probability.

theorem measure_le_xpehh {I₁ I₂ : Ω → ℝ} (h : IsExchangeablePair μ I₁ I₂) (h₁ : Measurable I₁)
    (h₂ : Measurable I₂) (t : ℝ) :
    μ {ω | t ≤ xpehh (I₁ ω) (I₂ ω)} = μ {ω | xpehh (I₁ ω) (I₂ ω) ≤ -t}

Uses 3

Statement usesExchangeable pair of statistics · Cross-population extended haplotype homozygosity (XP-EHH)

Proof usesEqual tails of the log ratio of an exchangeable pair

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.