Documentation

Lean 4 Proof

theorem shareFunction_le_one {w : Fin J → ℝ}
    (hw : ∀ j, 0 ≤ w j)
    (hpos : 0 < ∑ k : Fin J, w k) (j : Fin J) :
    shareFunction w j ≤ 1 := by
  have hsum := shareFunction_sum_one (ne_of_gt hpos)
  calc shareFunction w j
      ≤ ∑ k : Fin J, shareFunction w k :=
        Finset.single_le_sum (fun k _ => shareFunction_nonneg hw k) (Finset.mem_univ j)
    _ = 1 := hsum

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:113

Module Section

Ten Views of a Single Object:

In the same file