Documentation

Lean 4 Proof

theorem fastest_layer_regulation {phi_prev sigma_fast1 sigma_fast2 c : ℝ}
    (hs1 : sigma_fast1 ≠ 0) (hs2 : sigma_fast2 ≠ 0) :
    c * (phi_prev / sigma_fast1) * sigma_fast1 =
    c * (phi_prev / sigma_fast2) * sigma_fast2 := by
  have h1 : c * (phi_prev / sigma_fast1) * sigma_fast1 = c * phi_prev := by field_simp
  have h2 : c * (phi_prev / sigma_fast2) * sigma_fast2 = c * phi_prev := by field_simp
  rw [h1, h2]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:117

Module Section

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

In the same file