Documentation

Lean 4 Proof

theorem friction_from_vri
    (T χ σ_sq : ℝ) (hχ : 0 < χ) (hvri : σ_sq = T * χ) :
    σ_sq / χ = T := by
  rw [hvri, mul_div_cancel_right₀ T (ne_of_gt hχ)]

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:282

Module Section

## Corollary 3b.2: Mode-Specific Friction Measurement

In the same file