Documentation

Lean 4 Proof

theorem contestShare_is_shareFunction (a x : Fin J → ℝ)
    (ρ : ℝ) (j : Fin J) :
    contestShare a x ρ j =
    shareFunction (fun k => a k * x k ^ ρ) j :=
  rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:215

Module Section

Ten Views of a Single Object:

In the same file