Hardy–Weinberg law

DefinitionMendel's law of segregation#✓fully proved

Mendel's law of segregation: a parent with genotype g transmits its maternal allele g.1 or its paternal allele g.2, each with probability 1/2.

noncomputable def transmit (g : A × A) : PMF A :=
  (PMF.uniformFintype Bool).map fun b => cond b g.1 g.2

Uses 1 · Used by 4

Statement usesUniform distribution on a finite type

Used byLaw of a random gamete · Gamete law equals the allele frequency · Allele frequencies are conserved · Allele transmission law of a parental genotype

DefinitionLaw of a random gamete#✓fully proved

The law of a random gamete of a generation with genotype law G: pick a parent from G, then one of its two alleles by transmit. Its mass at a is the frequency of allele a (gamete_apply).

noncomputable def gamete (G : PMF (A × A)) : PMF A := G.bind transmit

Uses 1 · Used by 11

Statement usesMendel's law of segregation

Used byThe two allele frequencies sum to one · Gamete law equals the allele frequency · Allele frequencies are conserved · Deviation from Hardy–Weinberg proportions · Hardy–Weinberg proportions after one generation of random mating · Offspring genotype law under random union of gametes · Hardy–Weinberg proportions · Hardy–Weinberg frequency \(q^2\) of the aa homozygote · Hardy–Weinberg frequency \(2pq\) of the heterozygote · Hardy–Weinberg equilibrium · Hardy–Weinberg frequency \(p^2\) of the AA homozygote

DefinitionOffspring genotype law under random union of gametes#✓fully proved

The offspring genotype law under random union of gametes: the maternal and paternal alleles are independent gametes of the parental generation.

noncomputable def offspring (G : PMF (A × A)) : PMF (A × A) :=
  (gamete G).bind fun a => (gamete G).map (Prod.mk a)

Uses 1 · Used by 7

Statement usesLaw of a random gamete

Used byAllele frequencies are conserved · Hardy–Weinberg proportions after one generation of random mating · Hardy–Weinberg proportions · Hardy–Weinberg frequency \(q^2\) of the aa homozygote · Hardy–Weinberg frequency \(2pq\) of the heterozygote · Hardy–Weinberg equilibrium · Hardy–Weinberg frequency \(p^2\) of the AA homozygote

TheoremAllele transmission law of a parental genotype#✓fully proved

transmit g puts mass 1/2 on each of the two alleles of g (mass 1 on a for a homozygote g = (a, a)).

theorem transmit_apply [DecidableEq A] (g : A × A) (a : A) :
    transmit g a = (if g.1 = a then 2⁻¹ else 0) + (if g.2 = a then 2⁻¹ else 0)

Uses 2 · Used by 1

Statement usesMendel's law of segregation

Proof usesUniform distribution on a finite type

Used byGamete law equals the allele frequency

TheoremGamete law equals the allele frequency#✓fully proved

The gamete law is the allele frequency: gamete G a = ½ ∑ b, G (a, b) + ½ ∑ b, G (b, a), half the expected number of copies of a in a parental genotype.

theorem gamete_apply [Fintype A] (G : PMF (A × A)) (a : A) :
    gamete G a = 2⁻¹ * ∑ b, G (a, b) + 2⁻¹ * ∑ b, G (b, a)

Uses 3

Statement usesLaw of a random gamete

Proof usesMendel's law of segregation · Allele transmission law of a parental genotype

TheoremHardy–Weinberg proportions#✓fully proved

Hardy–Weinberg proportions (Hardy 1908, Weinberg 1908): after one generation of random mating the genotype law is the product p ⊗ p of the parental allele frequencies p = gamete G.

theorem offspring_apply (G : PMF (A × A)) (a b : A) :
    offspring G (a, b) = gamete G a * gamete G b

Uses 2 · Used by 3

Statement usesLaw of a random gamete · Offspring genotype law under random union of gametes

Used byHardy–Weinberg frequency \(q^2\) of the aa homozygote · Hardy–Weinberg frequency \(2pq\) of the heterozygote · Hardy–Weinberg frequency \(p^2\) of the AA homozygote

TheoremAllele frequencies are conserved#✓fully proved

Allele frequencies are conserved under random mating: the gamete law of the offspring equals that of the parents.

theorem gamete_offspring (G : PMF (A × A)) : gamete (offspring G) = gamete G

Uses 4 · Used by 2

Statement usesLaw of a random gamete · Offspring genotype law under random union of gametes

Proof usesMendel's law of segregation · Uniform distribution on a finite type

Used byHardy–Weinberg proportions after one generation of random mating · Hardy–Weinberg equilibrium

TheoremHardy–Weinberg equilibrium#✓fully proved

The Hardy–Weinberg proportions reached after one generation of random mating are a fixed point of random mating.

theorem offspring_offspring (G : PMF (A × A)) : offspring (offspring G) = offspring G

Uses 3

Statement usesOffspring genotype law under random union of gametes

Proof usesLaw of a random gamete · Allele frequencies are conserved

TheoremThe two allele frequencies sum to one#✓fully proved

The two allele frequencies sum to one: p + q = 1.

theorem freq_true_add_freq_false (G : PMF (Bool × Bool)) :
    (gamete G true).toReal + (gamete G false).toReal = 1

Uses 1

Statement usesLaw of a random gamete

TheoremHardy–Weinberg frequency \(p^2\) of the AA homozygote#✓fully proved

After one generation of random mating the homozygote AA has frequency p².

theorem offspring_true_true (G : PMF (Bool × Bool)) :
    (offspring G (true, true)).toReal = (gamete G true).toReal ^ 2

Uses 3 · Used by 1

Statement usesLaw of a random gamete · Offspring genotype law under random union of gametes

Proof usesHardy–Weinberg proportions

Used byHardy–Weinberg proportions after one generation of random mating

TheoremHardy–Weinberg frequency \(q^2\) of the aa homozygote#✓fully proved

After one generation of random mating the homozygote aa has frequency q².

theorem offspring_false_false (G : PMF (Bool × Bool)) :
    (offspring G (false, false)).toReal = (gamete G false).toReal ^ 2

Uses 3

Statement usesLaw of a random gamete · Offspring genotype law under random union of gametes

Proof usesHardy–Weinberg proportions

TheoremHardy–Weinberg frequency \(2pq\) of the heterozygote#✓fully proved

After one generation of random mating the (unordered) heterozygote Aa, i.e. the two ordered genotypes (A, a) and (a, A), has frequency 2pq.

theorem offspring_heterozygote (G : PMF (Bool × Bool)) :
    (offspring G (true, false)).toReal + (offspring G (false, true)).toReal =
      2 * (gamete G true).toReal * (gamete G false).toReal

Uses 3

Statement usesLaw of a random gamete · Offspring genotype law under random union of gametes

Proof usesHardy–Weinberg proportions

DefinitionDeviation from Hardy–Weinberg proportions#✓fully proved

The deviation D = P(AA) - p² of a biallelic genotype law from Hardy–Weinberg proportions, where p is the frequency of allele A (true).

noncomputable def hwDeviation (G : PMF (Bool × Bool)) : ℝ :=
  (G (true, true)).toReal - (gamete G true).toReal ^ 2

Uses 1 · Used by 1

Statement usesLaw of a random gamete

Used byHardy–Weinberg proportions after one generation of random mating

TheoremHardy–Weinberg proportions after one generation of random mating#✓fully proved

The deviation from Hardy–Weinberg proportions vanishes after one generation of random mating, whatever the parental genotype law.

theorem hwDeviation_offspring (G : PMF (Bool × Bool)) : hwDeviation (offspring G) = 0

Uses 5

Statement usesDeviation from Hardy–Weinberg proportions · Offspring genotype law under random union of gametes

Proof usesLaw of a random gamete · Allele frequencies are conserved · Hardy–Weinberg frequency \(p^2\) of the AA homozygote

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.