Prove2Me

Monotonicity of the scalar envelope

Proved
HlawkaSchatten.DiagonalConstruction.antitoneOn_scalarEnvelope

by savarin · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexityhlawka-schattenmonotonicityreal-analysisscalar-envelope

For a real exponent p≥1p\ge1 and q∈[0,1)q\in[0,1), define the scalar envelope root

ρp(q)=(1+qp2)1/p\rho_p(q) = \Bigl(\tfrac{1+q^p}{2}\Bigr)^{1/p}

and the scalar envelope

fp(q)  =  1−q2(1−ρp(q)).f_p(q) \;=\; \frac{1-q}{2\bigl(1-\rho_p(q)\bigr)}.

The theorem states that fpf_p is antitone (order-reversing, i.e. non-increasing) on the half-open interval [0,1)[0,1): for 0≤r≤q<10\le r\le q<1,

fp(q)  ≤  fp(r).f_p(q) \;\le\; f_p(r).

Elsewhere in the diagonal construction, fpf_p evaluated at qq equal to a normalized total norm ∥x+y+z∥p\|x+y+z\|_p is used as an upper bound on the ratio of the triple deficit to the pair-deficit sum of a normalized triple x,y,zx,y,z. Because fpf_p is antitone, a lower bound on qq then yields an upper bound on that ratio via fp(q)f_p(q); comparing this against the value of fpf_p at a fixed reference point is what confines a hypothetical strict counterexample's normalized total norm to a range below that reference point.

Preamble
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_ScalarBounds
import Mathlib.Analysis.Convex.Deriv
import Mathlib.Analysis.Convex.Function
import Mathlib.Analysis.Convex.Jensen
import Mathlib.Analysis.Convex.SpecificFunctions.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.NormPow
import Mathlib.Analysis.Normed.Lp.PiLp
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Real.Basic
import Mathlib.Data.Sign.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Topology.Instances.Sign
import Mathlib.Topology.Order.Compact

/-
Copyright (c) 2026 Ezzeri Esa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ezzeri Esa
-/

/-! # Monotonicity of the scalar envelope -/

open HlawkaSchatten.DiagonalConstruction
Formal statement
theorem HlawkaSchatten.DiagonalConstruction.antitoneOn_scalarEnvelope {p : ℝ} (hp : 1 ≤ p) :
    AntitoneOn (scalarEnvelope p) (Set.Ico 0 1) := by sorry
Source
https://github.com/savarin/hlawka-schatten/blob/79aa498bfcf7b22bd91d771fb32ec278e2d4704b/HlawkaSchatten/DiagonalConstruction/ScalarEnvelope.lean#L59-L87
Human review

  • Endorsed by Shuze Chen · Sep 29, 2026

    Confirmed by the moderator at approval.

  • Endorsed by savarin · Sep 29, 2026

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

  • Endorsed by marwahaha · Sep 30, 2026

View graph