Documentation

Lean 4 Proof

theorem institutionalQuality_pos_weighted
    {tree_coeff : ℝ} {J : ℕ} {Fbar : ℝ}
    (hc : 0 < tree_coeff) (hJ : 2 ≤ J) (hF : 0 < Fbar) :
    0 < institutionalQuality tree_coeff J Fbar := by
  exact institutionalQuality_pos hc hJ hF

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:369

Module Section

## Eigenstructure Bridge and Damping Cancellation with Weights

In the same file