Basis theorem for f-statistics

DefinitionPer-locus f4 form#✓fully proved

The per-locus f4 form x ↦ (x A - x B) * (x C - x D) on frequency vectors x : P → ℝ.

def f4Form (A B C D : P) : (P → ℝ) → ℝ := fun x => (x A - x B) * (x C - x D)

Used by 9

Used bySpace spanned by the per-locus f-statistics · Per-locus f2 form as a special f4 form · Every f2 form lies in the f-statistic space · Per-locus f3 form · f4 statistic as the integral of the f4 form · Polarization identity for the per-locus f4 form · Every f4 form lies in the f-statistic space · Linear independence of Patterson's f3 basis · Patterson's f2 basis spans the f-statistic space

DefinitionPer-locus f2 form#✓fully proved

The per-locus f2 form x ↦ (x A - x B) ^ 2.

def f2Form (A B : P) : (P → ℝ) → ℝ := fun x => (x A - x B) ^ 2

Used by 11

Used bySymmetry of the per-locus f2 form · Per-locus f2 form in terms of f3 forms with a base population · Per-locus f2 form as a special f4 form · Every f2 form lies in the f-statistic space · Per-locus f2 form of a population with itself is zero · Polarization identity for the per-locus f4 form · Dimension of the f-statistic space is n choose 2 · Integral of a linear combination of f2 forms · Linear independence of Patterson's f2 basis · Patterson's f2 basis spans the f-statistic space · Patterson's f3 basis spans the f-statistic space

DefinitionPer-locus f3 form#✓fully proved

The per-locus f3 form x ↦ (x C - x A) * (x C - x B).

def f3Form (C A B : P) : (P → ℝ) → ℝ := f4Form C A C B

Uses 1 · Used by 6

Statement usesPer-locus f4 form

Used byPer-locus f2 form in terms of f3 forms with a base population · Per-locus f3 form is symmetric in its sources · Every f3 form lies in the f-statistic space · Per-locus f3 form vanishes when target equals first source · Linear independence of Patterson's f3 basis · Patterson's f3 basis spans the f-statistic space

TheoremPer-locus f2 form as a special f4 form#✓fully proved

f2Form A B = f4Form A B A B.

theorem f2Form_eq_f4Form (A B : P) : f2Form A B = f4Form A B A B

Uses 2 · Used by 1

Statement usesPer-locus f2 form · Per-locus f4 form

Used byEvery f2 form lies in the f-statistic space

DefinitionSpace spanned by the per-locus f-statistics#✓fully proved

The space V_F spanned by all per-locus f-statistics (all f4Form; f2Form and f3Form are special cases).

noncomputable def fSpace (P : Type*) : Submodule ℝ ((P → ℝ) → ℝ) :=
  Submodule.span ℝ (Set.range fun q : P × P × P × P => f4Form q.1 q.2.1 q.2.2.1 q.2.2.2)

Uses 1 · Used by 6

Statement usesPer-locus f4 form

Used byEvery f2 form lies in the f-statistic space · Every f3 form lies in the f-statistic space · Every f4 form lies in the f-statistic space · Dimension of the f-statistic space is n choose 2 · Patterson's f2 basis spans the f-statistic space · Patterson's f3 basis spans the f-statistic space

TheoremEvery f4 form lies in the f-statistic space#✓fully proved

Every f4Form lies in V_F.

theorem f4Form_mem_fSpace (A B C D : P) : f4Form A B C D ∈ fSpace P

Uses 2 · Used by 2

Statement usesPer-locus f4 form · Space spanned by the per-locus f-statistics

Used byEvery f2 form lies in the f-statistic space · Every f3 form lies in the f-statistic space

TheoremEvery f2 form lies in the f-statistic space#✓fully proved

Every f2Form lies in V_F.

theorem f2Form_mem_fSpace (A B : P) : f2Form A B ∈ fSpace P

Uses 5 · Used by 1

Statement usesPer-locus f2 form · Space spanned by the per-locus f-statistics

Proof usesPer-locus f2 form as a special f4 form · Per-locus f4 form · Every f4 form lies in the f-statistic space

Used byPatterson's f2 basis spans the f-statistic space

TheoremEvery f3 form lies in the f-statistic space#✓fully proved

Every f3Form lies in V_F.

theorem f3Form_mem_fSpace (C A B : P) : f3Form C A B ∈ fSpace P

Uses 3 · Used by 1

Statement usesPer-locus f3 form · Space spanned by the per-locus f-statistics

Proof usesEvery f4 form lies in the f-statistic space

Used byPatterson's f3 basis spans the f-statistic space

Theoremf4 statistic as the integral of the f4 form#✓fully proved

The f4 statistic is the integral of the f4 form of the frequency vector.

theorem f4_eq_integral_f4Form {Ω : Type*} {m : MeasurableSpace Ω} (μ : Measure Ω)
    (p : P → Ω → ℝ) (A B C D : P) :
    f4 μ p A B C D = ∫ ω, f4Form A B C D (fun X => p X ω) ∂μ

Uses 2

Statement usesf4 statistic · Per-locus f4 form

TheoremIntegral of a linear combination of f2 forms#✓fully proved

A linear combination of f2 forms integrates to the same linear combination of f2 statistics, for square-integrable frequencies.

theorem integral_sum_smul_f2Form {Ω ι : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    {p : P → Ω → ℝ} (hp : ∀ X, MemLp (p X) 2 μ) (s : Finset ι) (c : ι → ℝ) (A B : ι → P) :
    ∫ ω, (∑ i ∈ s, c i • f2Form (A i) (B i)) (fun X => p X ω) ∂μ =
      ∑ i ∈ s, c i * f2 μ p (A i) (B i)

Uses 3

Statement usesf2 statistic · Per-locus f2 form

Proof usesSquare of a difference of square-integrable frequencies is integrable

TheoremSymmetry of the per-locus f2 form#✓fully proved

f2Form is symmetric.

theorem f2Form_comm (A B : P) : f2Form A B = f2Form B A

Uses 1 · Used by 1

Statement usesPer-locus f2 form

Used byPatterson's f2 basis spans the f-statistic space

TheoremPer-locus f2 form of a population with itself is zero#✓fully proved

f2Form A A = 0.

@[simp] theorem f2Form_self (A : P) : f2Form A A = 0

Uses 1 · Used by 1

Statement usesPer-locus f2 form

Used byPatterson's f2 basis spans the f-statistic space

TheoremPer-locus f3 form is symmetric in its sources#✓fully proved

f3Form is symmetric in its last two arguments.

theorem f3Form_comm (C A B : P) : f3Form C A B = f3Form C B A

Uses 1 · Used by 1

Statement usesPer-locus f3 form

Used byPatterson's f3 basis spans the f-statistic space

TheoremPer-locus f3 form vanishes when target equals first source#✓fully proved

f3Form C C B = 0.

@[simp] theorem f3Form_self_left (C B : P) : f3Form C C B = 0

Uses 1 · Used by 1

Statement usesPer-locus f3 form

Used byPatterson's f3 basis spans the f-statistic space

TheoremPolarization identity for the per-locus f4 form#✓fully proved

f4Form in terms of f2Form: the polarization identity behind f4_eq_f2.

theorem f4Form_eq (A B C D : P) :
    f4Form A B C D = (1 / 2 : ℝ) • (f2Form A D + f2Form B C - f2Form A C - f2Form B D)

Uses 2 · Used by 1

Statement usesPer-locus f2 form · Per-locus f4 form

Used byPatterson's f2 basis spans the f-statistic space

TheoremPer-locus f2 form in terms of f3 forms with a base population#✓fully proved

f2Form in terms of the f3 forms with base o.

theorem f2Form_eq_f3Form (o A B : P) :
    f2Form A B = f3Form o A A + f3Form o B B - (2 : ℝ) • f3Form o A B

Uses 2 · Used by 1

Statement usesPer-locus f2 form · Per-locus f3 form

Used byPatterson's f3 basis spans the f-statistic space

TheoremLinear independence of Patterson's f2 basis#✓fully proved

Patterson's f2 basis: the forms f2Form i j, i < j, are linearly independent.

theorem linearIndependent_f2Form :
    LinearIndependent ℝ (fun q : {q : P × P // q.1 < q.2} => f2Form q.1.1 q.1.2)

Uses 1 · Used by 1

Statement usesPer-locus f2 form

Used byDimension of the f-statistic space is n choose 2

TheoremPatterson's f2 basis spans the f-statistic space#✓fully proved

Patterson's f2 basis: the forms f2Form i j, i < j, span V_F, i.e. every f-statistic is a linear combination of the f2 Pᵢ Pⱼ, i < j.

theorem span_f2Form :
    Submodule.span ℝ (Set.range fun q : {q : P × P // q.1 < q.2} => f2Form q.1.1 q.1.2) =
      fSpace P

Uses 7 · Used by 2

Statement usesPer-locus f2 form · Space spanned by the per-locus f-statistics

Proof usesSymmetry of the per-locus f2 form · Every f2 form lies in the f-statistic space · Per-locus f2 form of a population with itself is zero · Per-locus f4 form · Polarization identity for the per-locus f4 form

Used byDimension of the f-statistic space is n choose 2 · Patterson's f3 basis spans the f-statistic space

TheoremLinear independence of Patterson's f3 basis#✓fully proved

Patterson's f3 basis with base population o: the forms f3Form o i j with i ≤ j, i ≠ o, j ≠ o are linearly independent.

theorem linearIndependent_f3Form (o : P) :
    LinearIndependent ℝ
      (fun q : {q : P × P // q.1 ≤ q.2 ∧ q.1 ≠ o ∧ q.2 ≠ o} => f3Form o q.1.1 q.1.2)

Uses 2

Statement usesPer-locus f3 form

Proof usesPer-locus f4 form

TheoremPatterson's f3 basis spans the f-statistic space#✓fully proved

Patterson's f3 basis with base population o: the forms f3Form o i j with i ≤ j, i ≠ o, j ≠ o span V_F.

theorem span_f3Form (o : P) :
    Submodule.span ℝ
        (Set.range fun q : {q : P × P // q.1 ≤ q.2 ∧ q.1 ≠ o ∧ q.2 ≠ o} =>
          f3Form o q.1.1 q.1.2) =
      fSpace P

Uses 8

Statement usesPer-locus f3 form · Space spanned by the per-locus f-statistics

Proof usesPer-locus f2 form · Per-locus f2 form in terms of f3 forms with a base population · Per-locus f3 form is symmetric in its sources · Every f3 form lies in the f-statistic space · Per-locus f3 form vanishes when target equals first source · Patterson's f2 basis spans the f-statistic space

TheoremDimension of the f-statistic space is n choose 2#✓fully proved

The f-statistics of n populations span a space of dimension n choose 2. (A linear order on the populations, used to index the f2 basis, is chosen in the proof.)

theorem finrank_fSpace [Fintype P] : Module.finrank ℝ (fSpace P) = (Fintype.card P).choose 2

Uses 4

Statement usesSpace spanned by the per-locus f-statistics

Proof usesPer-locus f2 form · Linear independence of Patterson's f2 basis · Patterson's f2 basis spans the f-statistic space

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.