Breeder's equation

6 fully proved

Breeder

StructureLinear parent–offspring regression model#✓fully proved

The linear parent–offspring model on a population described by a probability measure μ: the parental (mid-parent) value parent and the offspring value offspring are integrable, mean is the population mean of the parental value, and the offspring value regresses linearly on the parental value, 𝔼[O | P] = mean + h2 * (P - mean) (equivalently O = mean + h2 (P - mean) + e with 𝔼[e | P] = 0). Here h2 is the heritability.

MathlibExt.Biology.StatisticalGenetics.Breeder.Model · 20 lines

structure Model (μ : Measure Ω) [IsProbabilityMeasure μ] where
  /-- The population mean `μ` of the parental value. -/
  mean : ℝ
  /-- The heritability `h²`: the slope of the offspring-on-parent regression. -/
  h2 : ℝ
  /-- The parental (mid-parent) value `P`. -/
  parent : Ω → ℝ
  /-- The offspring value `O`. -/
  offspring : Ω → ℝ
  /-- The parental value is measurable. -/
  measurable_parent : Measurable parent
  /-- The parental value is integrable. -/
  integrable_parent : Integrable parent μ
  /-- The offspring value is integrable. -/
  integrable_offspring : Integrable offspring μ
  /-- `mean` is the population mean of the parental value: `𝔼[P] = μ`. -/
  integral_parent : ∫ ω, parent ω ∂μ = mean
  /-- Linear regression: `𝔼[O | P] = μ + h² (P - μ)`. -/
  condExp_offspring : μ[offspring | MeasurableSpace.comap parent inferInstance] =ᵐ[μ]
    fun ω => mean + h2 * (parent ω - mean)

Used by 5

Used byResponse to selection · Breeder's equation · Selecting the whole population gives zero response · Selection differential · Selecting the whole population gives zero selection differential

Model

DefinitionSelection differential#✓fully proved

The selection differential S = 𝔼[P | selected] - μ of the selected group s.

noncomputable def selectionDifferential (s : Set Ω) : ℝ := ∫ ω, M.parent ω ∂μ[|s] - M.mean

Uses 1 · Used by 3

Statement usesLinear parent–offspring regression model

Used byBreeder's equation · Selecting the whole population gives zero response · Selecting the whole population gives zero selection differential

DefinitionResponse to selection#✓fully proved

The response to selection R = 𝔼[O | selected] - μ: the mean offspring value of the selected parents, relative to the population mean.

noncomputable def response (s : Set Ω) : ℝ := ∫ ω, M.offspring ω ∂μ[|s] - M.mean

Uses 1 · Used by 2

Statement usesLinear parent–offspring regression model

Used byBreeder's equation · Selecting the whole population gives zero response

TheoremBreeder's equation#✓fully proved

The breeder's equation (Lush 1937): if the selected group s is determined by the parental value (an event of σ(P)) and has positive mass, the response to selection is the heritability times the selection differential, R = h² S.

theorem response_eq {s : Set Ω}
    (hs : MeasurableSet[MeasurableSpace.comap M.parent inferInstance] s) (hs0 : μ s ≠ 0) :
    M.response s = M.h2 * M.selectionDifferential s

Uses 3 · Used by 1

Statement usesLinear parent–offspring regression model · Response to selection · Selection differential

Used bySelecting the whole population gives zero response

TheoremSelecting the whole population gives zero selection differential#✓fully proved

Selecting the whole population gives no selection differential, S = 0.

theorem selectionDifferential_univ : M.selectionDifferential Set.univ = 0

Uses 2 · Used by 1

Statement usesLinear parent–offspring regression model · Selection differential

Used bySelecting the whole population gives zero response

TheoremSelecting the whole population gives zero response#✓fully proved

Selecting the whole population gives no response, R = 0.

theorem response_univ : M.response Set.univ = 0

Uses 5

Statement usesLinear parent–offspring regression model · Response to selection

Proof usesBreeder's equation · Selection differential · Selecting the whole population gives zero selection differential

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.