Even powers remove absolute values

Definition

KLSModular_BrownianMotion_Auxiliary_Nat

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-brownianmotion

Vendored from RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 under Apache-2.0. pow_two_mul_abs states that for a linearly ordered strict ordered ring, $|a|^{2n}=a^{2n}$ for every natural number $n$ .

Original module imports

public import Mathlib.Algebra.Order.Floor.Semiring
public import Mathlib.Algebra.Order.Ring.Abs

Original declaration excerpt

Shown in the original module context.

lemma pow_two_mul_abs {α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (n : ℕ) (a : α) :
    |a| ^ (2 * n) = a ^ (2 * n) :=
  Even.pow_abs ⟨n, two_mul n⟩ a

Module navigation

Project result: The KLS conjecture.

Original module · BrownianMotion.Auxiliary.Nat · Frozen source 408915f.

Definition code

import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Algebra.Order.Ring.Abs

-- Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (upstream path BrownianMotion/Auxiliary/Nat.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
section
lemma pow_two_mul_abs {α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (n : ℕ) (a : α) :
    |a| ^ (2 * n) = a ^ (2 * n) :=
  Even.pow_abs ⟨n, two_mul n⟩ a

Source

Lean source: https://github.com/RemyDegenne/brownian-motion/blob/a7ad7af662044313bc80a7c0756360fb3745f931/BrownianMotion/Auxiliary/Nat.lean#L8-L10 (repository human-ai-mathematics/kls-lean, commit 408915f, module `BrownianMotion.Auxiliary.Nat`, definition bundle `KLSModular_BrownianMotion_Auxiliary_Nat`; the repository is private at upload time). Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph