Documentation

Lean 4 Proof

theorem vri_consistency_test
    (T χ₁ χ₂ σ_sq₁ σ_sq₂ : ℝ)
    (hχ₁ : 0 < χ₁) (hχ₂ : 0 < χ₂)
    (hvri₁ : σ_sq₁ = T * χ₁) (hvri₂ : σ_sq₂ = T * χ₂) :
    σ_sq₁ / χ₁ = σ_sq₂ / χ₂ := by
  rw [hvri₁, hvri₂]
  field_simp

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:270

Module Section

## Theorem 3b.2: Weighted VRI (merged from WeightedVRI.lean)

In the same file