Documentation

Lean 4 Proof

theorem rho_renyi_correspondence_support {J : ℕ} (hJ : 0 < J)
    (p : Fin J → ℝ) (hsum : ∑ j, p j = 1) :
    1 / (↑J : ℝ) ≤ ∑ j, (p j) ^ 2 :=
  sum_sq_ge_inv_card hJ p hsum

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:67

Module Section

Aggregation-invariant class results from Paper 1, Section 5:

In the same file