Documentation

Lean 4 Proof

theorem damping_cancellation_weight_independent
    (c_n phi sigma_n : ℝ) (hσ : sigma_n ≠ 0) :
    c_n * (phi / sigma_n) * sigma_n = c_n * phi := by
  field_simp

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:377

Module Section

## Eigenstructure Bridge and Damping Cancellation with Weights

In the same file