Documentation

Lean 4 Proof

theorem T_cross_sectional {eps_i eps_j dHi dHj T mu : ℝ}
    (hdH : dHi ≠ dHj)
    (hFOC_i : eps_i = T * dHi + mu)
    (hFOC_j : eps_j = T * dHj + mu) :
    T = (eps_i - eps_j) / (dHi - dHj) := by
  have h : eps_i - eps_j = T * (dHi - dHj) := by linarith
  rw [h, mul_div_cancel_right₀ T (sub_ne_zero.mpr hdH)]

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:58

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file