Documentation

Lean 4 Proof

theorem onsager_reciprocity {N : ℕ} (χ : Fin N → Fin N → ℝ)
    (hχ : ∀ i j, χ i j = χ j i) (i j : Fin N) :
    χ i j = χ j i := hχ i j

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:410

Module Section

### Kramers Escape Rate

In the same file