Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Entropy and adjacency mass

Lax263307.Entropy · concepts/Lax263307/Entropy.lean · lax-263307

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    For a probability vector π\pi on nn vertices, its entropy in bits is

    H(π)=−∑vπvlog⁡2πv,H(\pi)=-\sum_v\pi_v\log_2\pi_v,

    with zero summands at zero probabilities. Its adjacency mass in a graph GG is

    ∑u,v: uv∈E(G)πuπv,\sum_{u,v:\,uv\in E(G)}\pi_u\pi_v,

    where ordered adjacent pairs are counted, so each edge contributes twice.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
    2import Mathlib.Analysis.SpecialFunctions.Log.Base
    3import Mathlib.Combinatorics.SimpleGraph.Basic
    4
    5/-!
    6---
    7title: Entropy and adjacency mass
    8type: definition
    9---
    10For a probability vector π\pi on nn vertices, its entropy in bits is
    11H(π)=−∑vπvlog⁡2πv,H(\pi)=-\sum_v\pi_v\log_2\pi_v,
    12with zero summands at zero probabilities. Its adjacency mass in a graph GG is
    13∑u,v: uv∈E(G)πuπv,\sum_{u,v:\,uv\in E(G)}\pi_u\pi_v,
    14where ordered adjacent pairs are counted, so each edge contributes twice.
    15
    16# Formalization notes
    17
    18The auxiliary natural-log entropy differs by the positive factor ln⁡2\ln2.
    19Both definitions use mathlib's `negMulLog`, whose value at zero is zero.
    20The adjacency mass is an ordered sum, avoiding choices of edge orientations.
    21-/
    22
    23namespace Lax263307.Entropy
    24
    25/-- A nonnegative vector with total mass one. -/
    26def IsProbability {n : ℕ} (π : Fin n → ℝ) : Prop :=
    27 (∀ v, 0 ≤ π v) ∧ (∑ v, π v) = 1
    28
    29/-- Entropy measured with natural logarithms. -/
    30noncomputable def naturalEntropy {n : ℕ} (π : Fin n → ℝ) : ℝ :=
    31 ∑ v, Real.negMulLog (π v)
    32
    33/-- Shannon entropy in bits. -/
    34noncomputable def entropy {n : ℕ} (π : Fin n → ℝ) : ℝ :=
    35 naturalEntropy π / Real.log 2
    36
    37/-- Total product probability of ordered adjacent vertex pairs. -/
    38noncomputable def adjacencyMass {n : ℕ} (G : SimpleGraph (Fin n))
    39 [DecidableRel G.Adj] (π : Fin n → ℝ) : ℝ :=
    40 ∑ u, ∑ v, if G.Adj u v then π u * π v else 0
    41
    42/-- Sum of endpoint-cost products over unordered edges. -/
    43noncomputable def edgeCost {n : ℕ} (G : SimpleGraph (Fin n))
    44 [DecidableRel G.Adj] (x : Fin n → ℝ) : ℝ :=
    45 adjacencyMass G x / 2
    46
    47end Lax263307.Entropy
    48
    Formalization notes

    The auxiliary natural-log entropy differs by the positive factor ln⁡2\ln2. Both definitions use mathlib's negMulLognegMulLog, whose value at zero is zero. The adjacency mass is an ordered sum, avoiding choices of edge orientations.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…