Documentation

Lean 4 Proof

theorem crossLevelDistQF_nonneg (P : HierarchicalPartition J N) (v : Fin J → ℝ) :
    0 ≤ crossLevelDistQF P v := by
  apply mul_nonneg (by norm_num : (0:ℝ) ≤ 1/2)
  apply Finset.sum_nonneg; intro j _
  apply Finset.sum_nonneg; intro k _
  apply mul_nonneg _ (sq_nonneg _)
  by_cases h : P.level j ≠ P.level k <;> simp [h]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:301

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file