Documentation

Lean 4 Proof

theorem effectiveLevelCurvature_nonneg (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k)
    (P : HierarchicalPartition J N) (n : Fin N) :
    0 ≤ effectiveLevelCurvature net P n := by
  simp only [effectiveLevelCurvature, levelCoupling]
  split
  · exact le_refl 0
  · rename_i h; push_neg at h
    apply div_nonneg
    · apply Finset.sum_nonneg; intro j _
      apply Finset.sum_nonneg; intro k _
      by_cases hc : P.level j = n ∧ P.level k = n ∧ j ≠ k
      · simp [hc, hw j k]
      · simp [hc]
    · have hJn : (2 : ℝ) ≤ ↑(levelSize P n) := by
        exact_mod_cast (show 2 ≤ levelSize P n by omega)
      exact le_of_lt (mul_pos (by linarith) (by linarith))

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:259

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file