Documentation

Lean 4 Proof

theorem qExpAllocation_is_shareFunction (q T : ℝ)
    (ε : Fin J → ℝ) (j : Fin J) :
    qExpAllocation J q T ε j =
    shareFunction (fun k => qExp q (ε k / T)) j := by
  simp only [qExpAllocation, shareFunction]

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:225

Module Section

Ten Views of a Single Object:

In the same file