Documentation

Lean 4 Proof

theorem shareFunction_iia [NeZero J] {w : Fin J → ℝ}
    (hw : ∀ j, 0 < w j) (j k : Fin J) :
    shareFunction w j / shareFunction w k = w j / w k := by
  simp only [shareFunction]
  have hsum : (0 : ℝ) < ∑ i, w i :=
    Finset.sum_pos (fun i _ => hw i) Finset.univ_nonempty
  field_simp [ne_of_gt hsum, ne_of_gt (hw k)]

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:90

Module Section

Ten Views of a Single Object:

In the same file