Intrinsic and extrinsic gene expression noise

DefinitionIntrinsic noise strength#✓fully proved

Two-reporter intrinsic noise strength η_int² = ⟨(X - Y)²⟩ / (2 ⟨X⟩⟨Y⟩).

noncomputable def intrinsicNoiseSq (μ : Measure[m₀] Ω) (X Y : Ω → ℝ) : ℝ :=
  μ[(X - Y) ^ 2] / (2 * (μ[X] * μ[Y]))

Used by 3

Used byTwo-reporter formula for intrinsic noise · Total noise splits into intrinsic and extrinsic parts · Two-reporter decomposition

DefinitionExtrinsic noise strength#✓fully proved

Two-reporter extrinsic noise strength η_ext² = (⟨X Y⟩ - ⟨X⟩⟨Y⟩) / (⟨X⟩⟨Y⟩).

noncomputable def extrinsicNoiseSq (μ : Measure[m₀] Ω) (X Y : Ω → ℝ) : ℝ :=
  (μ[X * Y] - μ[X] * μ[Y]) / (μ[X] * μ[Y])

Used by 3

Used byTwo-reporter formula for extrinsic noise · Total noise splits into intrinsic and extrinsic parts · Two-reporter decomposition

DefinitionTotal noise strength#✓fully proved

Two-reporter total noise strength η_tot² = (⟨X² + Y²⟩ / 2 - ⟨X⟩⟨Y⟩) / (⟨X⟩⟨Y⟩).

noncomputable def totalNoiseSq (μ : Measure[m₀] Ω) (X Y : Ω → ℝ) : ℝ :=
  (μ[X ^ 2 + Y ^ 2] / 2 - μ[X] * μ[Y]) / (μ[X] * μ[Y])

Used by 2

Used byTotal noise splits into intrinsic and extrinsic parts · Two-reporter decomposition

TheoremTwo-reporter decomposition#✓fully proved

Two-reporter decomposition (Swain et al. 2002; Elowitz et al. 2002): for any square-integrable reporters, η_tot² = η_int² + η_ext².

theorem totalNoiseSq_eq_add (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    totalNoiseSq μ X Y = intrinsicNoiseSq μ X Y + extrinsicNoiseSq μ X Y

Uses 3 · Used by 1

Statement usesExtrinsic noise strength · Intrinsic noise strength · Total noise strength

Used byTotal noise splits into intrinsic and extrinsic parts

StructureIdentical reporter pair#✓fully proved

Two reporters of the same gene given the extrinsic σ-algebra m: equal conditional means, equal conditional second moments, and conditionally uncorrelated. Conditional independence with identical conditional laws given m implies these three conditions.

structure IsIdenticalReporterPair (m : MeasurableSpace Ω) (μ : Measure[m₀] Ω)
    (X Y : Ω → ℝ) : Prop where
  condExp_eq : μ[X | m] =ᵐ[μ] μ[Y | m]
  condExp_sq_eq : μ[X ^ 2 | m] =ᵐ[μ] μ[Y ^ 2 | m]
  condExp_mul : μ[X * Y | m] =ᵐ[μ] μ[X | m] * μ[Y | m]

Used by 6

Used byCovariance of identical reporters equals extrinsic variance · Two-reporter formula for extrinsic noise · Identical reporters have equal means · Half mean squared reporter difference equals intrinsic variance · Two-reporter formula for intrinsic noise · Total noise splits into intrinsic and extrinsic parts

TheoremIdentical reporters have equal means#✓fully proved

Identical reporters have the same mean.

theorem IsIdenticalReporterPair.integral_eq (hm : m ≤ m₀) (h : IsIdenticalReporterPair m μ X Y) :
    μ[X] = μ[Y]

Uses 1 · Used by 4

Statement usesIdentical reporter pair

Used byCovariance of identical reporters equals extrinsic variance · Two-reporter formula for extrinsic noise · Half mean squared reporter difference equals intrinsic variance · Two-reporter formula for intrinsic noise

TheoremCovariance of identical reporters equals extrinsic variance#✓fully proved

For identical reporters the covariance is the extrinsic variance: Cov(X, Y) = Var(E[X | m]).

theorem IsIdenticalReporterPair.covariance_eq_variance_condExp (hm : m ≤ m₀)
    (h : IsIdenticalReporterPair m μ X Y) (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    cov[X, Y; μ] = Var[μ[X | m]; μ]

Uses 2 · Used by 2

Statement usesIdentical reporter pair

Proof usesIdentical reporters have equal means

Used byTwo-reporter formula for extrinsic noise · Half mean squared reporter difference equals intrinsic variance

TheoremHalf mean squared reporter difference equals intrinsic variance#✓fully proved

For identical reporters half the mean squared difference is the intrinsic variance: ⟨(X - Y)²⟩ / 2 = ⟨Var(X | m)⟩.

theorem IsIdenticalReporterPair.integral_sub_sq_div_two_eq (hm : m ≤ m₀)
    (h : IsIdenticalReporterPair m μ X Y) (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    μ[(X - Y) ^ 2] / 2 = μ[Var[X; μ | m]]

Uses 3 · Used by 1

Statement usesIdentical reporter pair

Proof usesCovariance of identical reporters equals extrinsic variance · Identical reporters have equal means

Used byTwo-reporter formula for intrinsic noise

TheoremTwo-reporter formula for extrinsic noise#✓fully proved

The two-reporter extrinsic noise is Var(E[X | m]) / ⟨X⟩² (Swain et al. Eq. 8).

theorem IsIdenticalReporterPair.extrinsicNoiseSq_eq (hm : m ≤ m₀)
    (h : IsIdenticalReporterPair m μ X Y) (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    extrinsicNoiseSq μ X Y = Var[μ[X | m]; μ] / μ[X] ^ 2

Uses 4 · Used by 1

Statement usesIdentical reporter pair · Extrinsic noise strength

Proof usesCovariance of identical reporters equals extrinsic variance · Identical reporters have equal means

Used byTotal noise splits into intrinsic and extrinsic parts

TheoremTwo-reporter formula for intrinsic noise#✓fully proved

The two-reporter intrinsic noise is ⟨Var(X | m)⟩ / ⟨X⟩² (Swain et al. Eq. 8).

theorem IsIdenticalReporterPair.intrinsicNoiseSq_eq (hm : m ≤ m₀)
    (h : IsIdenticalReporterPair m μ X Y) (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    intrinsicNoiseSq μ X Y = μ[Var[X; μ | m]] / μ[X] ^ 2

Uses 4 · Used by 1

Statement usesIdentical reporter pair · Intrinsic noise strength

Proof usesIdentical reporters have equal means · Half mean squared reporter difference equals intrinsic variance

Used byTotal noise splits into intrinsic and extrinsic parts

TheoremTotal noise splits into intrinsic and extrinsic parts#✓fully proved

The two-reporter total noise is Var(X) / ⟨X⟩², and it splits into the intrinsic and extrinsic parts by the law of total variance.

theorem IsIdenticalReporterPair.totalNoiseSq_eq (hm : m ≤ m₀)
    (h : IsIdenticalReporterPair m μ X Y) (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
    totalNoiseSq μ X Y = Var[X; μ] / μ[X] ^ 2

Uses 7

Statement usesIdentical reporter pair · Total noise strength

Proof usesTwo-reporter formula for extrinsic noise · Two-reporter formula for intrinsic noise · Extrinsic noise strength · Intrinsic noise strength · Two-reporter decomposition

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.