Morphogen gradients and the French flag model

DefinitionDecay length of a morphogen gradient#✓fully proved

The decay length λ = √(D / k) of a morphogen with diffusion coefficient D and linear degradation rate k (both positive in the model).

noncomputable def decayLength (D k : ℝ) : ℝ :=
  √(D / k)

Used by 12

Used byPositivity of the decay length · Diffusion coefficient over squared decay length equals degradation rate · Uniqueness · Slope of the morphogen profile · Exponential profile is a bounded steady state · Steady-state exponential morphogen profile · Morphogen profile is strictly decreasing · Profile equals the threshold at the French-flag boundary · Source amplitude in terms of the decay length · French-flag boundary position for a threshold · Boundary shift · Doubling the source flux shifts boundaries by \(\lambda \log 2\)

DefinitionSteady-state exponential morphogen profile#✓fully proved

The steady-state gradient c(x) = (j / √(D k)) e^{-x/λ}, λ = √(D / k), for source flux j at x = 0. Meaningful for D, k > 0.

noncomputable def profile (D k j x : ℝ) : ℝ :=
  j / √(D * k) * exp (-x / decayLength D k)

Uses 1 · Used by 7

Statement usesDecay length of a morphogen gradient

Used byUniqueness · Slope of the morphogen profile · Exponential profile is a bounded steady state · French-flag regions · French-flag boundary · Morphogen profile is strictly decreasing · Profile equals the threshold at the French-flag boundary

DefinitionFrench-flag boundary position for a threshold#✓fully proved

The French-flag boundary for threshold θ: x_θ = λ log(c(0) / θ), where c(0) = j / √(D k). Meaningful for D, k, j, θ > 0; it is negative when θ > c(0) (no cell is above threshold).

noncomputable def thresholdPosition (D k j θ : ℝ) : ℝ :=
  decayLength D k * log (j / √(D * k) / θ)

Uses 1 · Used by 5

Statement usesDecay length of a morphogen gradient

Used byFrench-flag regions · French-flag boundary · Profile equals the threshold at the French-flag boundary · Boundary shift · Doubling the source flux shifts boundaries by \(\lambda \log 2\)

StructureBounded steady state of the synthesis–diffusion–degradation model#✓fully proved

A bounded steady state of the synthesis–diffusion–degradation model on [0, ∞), with c' = dc/dx: D c'' = k c for x > 0, c and c' continuous up to the source, source flux -D c'(0) = j, and c bounded on [0, ∞).

structure IsSteadyState (D k j : ℝ) (c c' : ℝ → ℝ) : Prop where
  hasDerivAt_conc : ∀ x, 0 < x → HasDerivAt c (c' x) x
  hasDerivAt_grad : ∀ x, 0 < x → HasDerivAt c' (k / D * c x) x
  continuousOn_conc : ContinuousOn c (Ici 0)
  continuousOn_grad : ContinuousOn c' (Ici 0)
  source_flux : -D * c' 0 = j
  bounded : ∃ B, ∀ x, 0 ≤ x → |c x| ≤ B

Used by 2

Used byUniqueness · Exponential profile is a bounded steady state

TheoremPositivity of the decay length#✓fully proved

The decay length is positive for positive D and k.

theorem decayLength_pos {D k : ℝ} (hD : 0 < D) (hk : 0 < k) : 0 < decayLength D k

Uses 1 · Used by 5

Statement usesDecay length of a morphogen gradient

Used byUniqueness · Exponential profile is a bounded steady state · Morphogen profile is strictly decreasing · Profile equals the threshold at the French-flag boundary · Source amplitude in terms of the decay length

TheoremDiffusion coefficient over squared decay length equals degradation rate#✓fully proved

D / λ² = k.

theorem div_decayLength_sq {D k : ℝ} (hD : 0 < D) (hk : 0 < k) :
    D / decayLength D k ^ 2 = k

Uses 1

Statement usesDecay length of a morphogen gradient

TheoremSource amplitude in terms of the decay length#✓fully proved

√(D k) = D / λ, so the source amplitude is c(0) = j λ / D.

theorem sqrt_mul_eq {D k : ℝ} (hD : 0 < D) (hk : 0 < k) :
    √(D * k) = D / decayLength D k

Uses 2 · Used by 2

Statement usesDecay length of a morphogen gradient

Proof usesPositivity of the decay length

Used byUniqueness · Exponential profile is a bounded steady state

TheoremSlope of the morphogen profile#✓fully proved

The profile has slope c'(x) = -c(x)/λ.

theorem hasDerivAt_profile (D k j x : ℝ) :
    HasDerivAt (profile D k j) (-profile D k j x / decayLength D k) x

Uses 2 · Used by 1

Statement usesDecay length of a morphogen gradient · Steady-state exponential morphogen profile

Used byExponential profile is a bounded steady state

TheoremExponential profile is a bounded steady state#✓fully proved

The exponential profile is a bounded steady state with source flux j.

theorem isSteadyState_profile {D k j : ℝ} (hD : 0 < D) (hk : 0 < k) :
    IsSteadyState D k j (profile D k j) (fun x ↦ -profile D k j x / decayLength D k)

Uses 6

Statement usesBounded steady state of the synthesis–diffusion–degradation model · Decay length of a morphogen gradient · Steady-state exponential morphogen profile

Proof usesPositivity of the decay length · Slope of the morphogen profile · Source amplitude in terms of the decay length

TheoremUniqueness#✓fully proved

Every bounded steady state with source flux j is the exponential profile on [0, ∞).

theorem eq_profile_of_isSteadyState {D k j : ℝ} (hD : 0 < D) (hk : 0 < k) {c c' : ℝ → ℝ}
    (hc : IsSteadyState D k j c c') {x : ℝ} (hx : 0 ≤ x) :
    c x = profile D k j x

Uses 5

Statement usesBounded steady state of the synthesis–diffusion–degradation model · Steady-state exponential morphogen profile

Proof usesDecay length of a morphogen gradient · Positivity of the decay length · Source amplitude in terms of the decay length

TheoremMorphogen profile is strictly decreasing#✓fully proved

The profile is strictly decreasing in x for a positive source.

theorem profile_strictAnti {D k j : ℝ} (hD : 0 < D) (hk : 0 < k) (hj : 0 < j) :
    StrictAnti (profile D k j)

Uses 3 · Used by 2

Statement usesSteady-state exponential morphogen profile

Proof usesDecay length of a morphogen gradient · Positivity of the decay length

Used byFrench-flag regions · French-flag boundary

TheoremProfile equals the threshold at the French-flag boundary#✓fully proved

The profile equals θ at the boundary x_θ.

theorem profile_thresholdPosition {D k j θ : ℝ} (hD : 0 < D) (hk : 0 < k) (hj : 0 < j)
    (hθ : 0 < θ) : profile D k j (thresholdPosition D k j θ) = θ

Uses 4 · Used by 2

Statement usesSteady-state exponential morphogen profile · French-flag boundary position for a threshold

Proof usesDecay length of a morphogen gradient · Positivity of the decay length

Used byFrench-flag regions · French-flag boundary

TheoremFrench-flag boundary#✓fully proved

For positive parameters and threshold θ, c(x) = θ exactly at x = x_θ = λ log(c(0)/θ).

theorem profile_eq_iff {D k j θ : ℝ} (hD : 0 < D) (hk : 0 < k) (hj : 0 < j) (hθ : 0 < θ)
    (x : ℝ) : profile D k j x = θ ↔ x = thresholdPosition D k j θ

Uses 4

Statement usesSteady-state exponential morphogen profile · French-flag boundary position for a threshold

Proof usesMorphogen profile is strictly decreasing · Profile equals the threshold at the French-flag boundary

TheoremFrench-flag regions#✓fully proved

A cell at x is at or above threshold θ iff it lies within the boundary x_θ: θ ≤ c(x) ↔ x ≤ x_θ.

theorem le_profile_iff {D k j θ : ℝ} (hD : 0 < D) (hk : 0 < k) (hj : 0 < j) (hθ : 0 < θ)
    (x : ℝ) : θ ≤ profile D k j x ↔ x ≤ thresholdPosition D k j θ

Uses 4

Statement usesSteady-state exponential morphogen profile · French-flag boundary position for a threshold

Proof usesMorphogen profile is strictly decreasing · Profile equals the threshold at the French-flag boundary

TheoremBoundary shift#✓fully proved

Scaling the source flux by a > 0 moves every French-flag boundary by λ log a.

theorem thresholdPosition_mul {D k j θ a : ℝ} (hj : 0 < j) (hD : 0 < D) (hk : 0 < k)
    (hθ : 0 < θ) (ha : 0 < a) :
    thresholdPosition D k (a * j) θ = thresholdPosition D k j θ + decayLength D k * log a

Uses 2 · Used by 1

Statement usesDecay length of a morphogen gradient · French-flag boundary position for a threshold

Used byDoubling the source flux shifts boundaries by \(\lambda \log 2\)

TheoremDoubling the source flux shifts boundaries by \(\lambda \log 2\)#✓fully proved

Doubling the source flux shifts every French-flag boundary away from the source by exactly λ log 2.

theorem thresholdPosition_two_mul {D k j θ : ℝ} (hj : 0 < j) (hD : 0 < D) (hk : 0 < k)
    (hθ : 0 < θ) :
    thresholdPosition D k (2 * j) θ = thresholdPosition D k j θ + decayLength D k * log 2

Uses 3

Statement usesDecay length of a morphogen gradient · French-flag boundary position for a threshold

Proof usesBoundary shift

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.