Documentation

Lean 4 Proof

theorem escortDistribution_is_shareFunction (q : ℝ)
    (x : Fin J → ℝ) (j : Fin J) :
    escortDistribution J q x j = shareFunction (fun k => (x k) ^ q) j :=
  rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:164

Module Section

Ten Views of a Single Object:

In the same file