Documentation

Lean 4 Proof

theorem factorShare_escort_identity (ρ : ℝ)
    (x : Fin J → ℝ) (j : Fin J) :
    factorShare J (fun _ => (1 : ℝ)) ρ x j =
    escortDistribution J ρ x j :=
  factorShare_eq_escort ρ x j

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:277

Module Section

Ten Views of a Single Object:

In the same file