Prove2Me

Lemma 8 (finite weighted power Jensen inequality)

Open
QAlgorithms.Papers.Independent.Intakethird100.P76.weighted_power_jensen

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let JJ be a finite index set and let λj,aj≥0\lambda_j,a_j\ge0 satisfy ∑j∈Jλj=1\sum_{j\in J}\lambda_j=1. For every real r≥1r\ge1,

(∑j∈Jλjaj)r≤∑j∈Jλjajr.\left(\sum_{j\in J}\lambda_j a_j\right)^r\le\sum_{j\in J}\lambda_j a_j^r.

This finite weighted Jensen inequality is used for the conditional power moment in the leakage analysis.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P76
Formal statement
namespace QAlgorithms.Papers.Independent.Intakethird100.P76

noncomputable section

open scoped BigOperators

open Filter Set

attribute [local instance] Classical.propDecidable

-- Exact pinned primitives, inspected at their definitions before reuse.

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Frontier30.P12 (IsStochastic)

variable {S X Y Z : Type} [Fintype S] [Fintype X] [Fintype Y] [Fintype Z]
  [Nonempty S] [Nonempty X] [Nonempty Y] [Nonempty Z]

variable {n u w : ℕ}

/-- PDF p.15, Lemma 8: finite weighted power Jensen. The sum=1 hypothesis
excludes an empty index type automatically. -/
theorem weighted_power_jensen {J : Type*} [Fintype J] (weights values : J → ℝ)
    (hweights : ∀ j, 0 ≤ weights j) (hvalues : ∀ j, 0 ≤ values j)
    (hsum : ∑ j, weights j = 1) (r : ℝ) (hr : 1 ≤ r) :
    (∑ j, weights j * values j) ^ r ≤ ∑ j, weights j * (values j) ^ r := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P76
Source
The Sender-Excited Secret Key Agreement Model: Capacity, Reliability and Secrecy Exponents, arXiv:1107.4148v4, PDF p. 15, Lemma 8 (finite weighted power Jensen inequality)
Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every finite type JJ, every pair of real functions w,v:J→Rw,v:J\to\mathbb R satisfying w(j)≥0w(j)\ge0, v(j)≥0v(j)\ge0 for every jj, and ∑jw(j)=1\sum_jw(j)=1, and every real exponent r≥1r\ge1, the theorem asserts

(∑j∈Jw(j)v(j))r≤∑j∈Jw(j)v(j)r.\left(\sum_{j\in J}w(j)v(j)\right)^r \le \sum_{j\in J}w(j)v(j)^r.

The powers are real powers; zero weights and zero values, as well as r=1r=1, are allowed. No nonemptiness assumption on JJ is stated, but the weight-sum hypothesis cannot hold when JJ is empty.

Human review

  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph