Documentation

Lean 4 Proof

theorem overlap_weights_sum_one {M N : ℕ} (w : Fin M → Fin N → ℝ)
    (hw : ∀ j, ∑ n : Fin N, w j n = 1) (j : Fin M) :
    ∑ n : Fin N, overlapWeight w j n = 1 := hw j

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:311

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file