weighted_log_average
plain-language theorem explainer
Weighted average of the logarithms of ledger entries equals total log-charge divided by N. Variational dynamics proofs cite this to relate the conserved charge to per-entry log-ratios when applying Jensen bounds. The proof reduces directly by unfolding the log-charge definition, distributing the factor 1/N, and applying ring normalization.
Claim. For positive integer $N$ and configuration $c$ with $N$ positive real entries, the weighted average of the logarithms satisfies $$ (1/N) sum_i log(c_i) = L(c)/N, $$ where $L(c)$ denotes the total log-charge, defined as the sum of the individual logarithms.
background
The VariationalDynamics module formalizes the ledger update as constrained global minimization of total defect subject to conservation of the total log-ratio. A Configuration is a structure of $N$ positive real entries representing ledger ratios. The module states that the ledger conserves total log-ratio: sum log(x_i) is invariant; this sum is called the charge of the ledger. The identity equates the uniform weighted average of the logs to this charge divided by $N$.
proof idea
The proof unfolds the definition of log_charge, rewrites the sum via the distributive property of multiplication over summation, and concludes by ring normalization.
why it matters
This identity supplies the algebraic step for the total_defect_lower_bound theorem, which obtains the Jensen lower bound $N * Jlog(log_charge c / N) <= total_defect c$, and for the equality case theorem that forces constant configurations when equality holds. It encodes the conservation law of the total log-ratio in the ledger evolution principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.