Documentation

Lean 4 Proof

theorem T_measurement_vri {sigma_sq chi T : ℝ}
    (hchi : chi ≠ 0)
    (hVRI : sigma_sq = T * chi) :
    T = sigma_sq / chi := by
  rw [hVRI, mul_div_cancel_right₀ T hchi]

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:108

Module Section

Results 8-16: Variance-Response Identity and Early Warning

In the same file