Documentation

Lean 4 Proof

theorem welfare_independent_of_own_sigma_weighted
    (c_n phi_n : ℝ) (σ₁ σ₂ : ℝ) (hσ₁ : σ₁ ≠ 0) (hσ₂ : σ₂ ≠ 0) :
    c_n * (phi_n / σ₁) * σ₁ = c_n * (phi_n / σ₂) * σ₂ := by
  field_simp

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:383

Module Section

## Eigenstructure Bridge and Damping Cancellation with Weights

In the same file