Documentation

Lean 4 Proof

theorem welfare_independent_of_own_sigma {phi_prev sigma1 sigma2 c delta : ℝ}
    (hs1 : sigma1 ≠ 0) (hs2 : sigma2 ≠ 0) :
    c * (phi_prev / sigma1) * sigma1 * delta ^ 2 =
    c * (phi_prev / sigma2) * sigma2 * delta ^ 2 := by
  have h1 : c * (phi_prev / sigma1) * sigma1 = c * phi_prev := by field_simp
  have h2 : c * (phi_prev / sigma2) * sigma2 = c * phi_prev := by field_simp
  rw [h1, h2]

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:68

Module Section

Proposition 6, Theorem 9, Corollaries 1-2 and 4:

In the same file