Documentation

Lean 4 Proof

theorem shareFunction_coordinate_invariance
    (φ : ℝ → ℝ) (y : Fin J → ℝ) (j : Fin J) :
    shareFunction (fun k => φ (y k)) j =
    φ (y j) / ∑ k : Fin J, φ (y k) :=
  rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:507

Module Section

Ten Views of a Single Object:

In the same file