Documentation

Lean 4 Proof

theorem shareFunction_maximum_dominates [NeZero J]
    {w : Fin J → ℝ} (hw : ∀ j, 0 < w j)
    {j₀ : Fin J} (hmax : ∀ k, w k ≤ w j₀) :
    ∀ j, shareFunction w j ≤ shareFunction w j₀ := by
  intro j
  simp only [shareFunction]
  apply div_le_div_of_nonneg_right (hmax j)
  exact (Finset.sum_pos (fun i _ => hw i) Finset.univ_nonempty).le

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:543

Module Section

Ten Views of a Single Object:

In the same file