Coordinate permutation and coordinatewise rescaling in R^3 (orient)

Definition

HlawkaSchatten_DiagonalConstruction_Coordinates

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

hlawka-schattenpermutationsymmetry

For a permutation $e$ of $\{0,1,2\}$ , a real vector $s=(s_0,s_1,s_2)\in\mathbb{R}^3$ , and a vector $x\in\mathbb{R}^3$ , orient defines the vector obtained by permuting $x$ 's entries by $e$ and then multiplying entry $i$ by $s_i$ :

\mathrm{orient}(e,s,x)_i = s_i \cdot x_{e(i)}.

This packages, as a single map, the symmetry used to recover a shared coordinate pattern in the diagonal construction: permuting the three coordinates and multiplying by $s$ . orient itself places no restriction on $s$ ; lpNorm and the Hlawka deficit are unchanged under orient whenever every $|s_i|=1$ — a hypothesis of those invariance facts, not of orient itself — and it is that sign-flip case that lets a general configuration be reduced to a normal form (the cyclic sign pattern) without loss.

Definition code

import Mathlib.Analysis.Complex.ExponentialBounds
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.Abel
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
-/

/-! # Large pair coordinates and signed coordinate permutations -/

namespace HlawkaSchatten.DiagonalConstruction









/-- A simultaneous coordinate permutation and reflection. -/
def orient (e : Equiv.Perm (Fin 3)) (s : Fin 3 → ℝ) (x : Fin 3 → ℝ) : Fin 3 → ℝ :=
  fun i ↦ s i * x (e i)







end HlawkaSchatten.DiagonalConstruction

Source

https://github.com/savarin/hlawka-schatten/blob/79aa498bfcf7b22bd91d771fb32ec278e2d4704b/HlawkaSchatten/DiagonalConstruction/Coordinates.lean#L98-L100

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