Coherent cpow half sub one norm le

Proved

D1Bound5.coherent_cpow_half_sub_one_norm_le

by tp · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

A geometric bound for the actual principal half-power remainder. This follows from its convergent binomial series and the coefficient bound |b_n| <= 1/2, without selecting a new square-root sign.

Preamble

import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Analysis.Analytic.Binomial
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.Data.Finset.Insert
import Mathlib.Data.Sym.Basic
import Mathlib.Data.Sym.Card
import Mathlib.LinearAlgebra.Lagrange
import Mathlib.RingTheory.Binomial
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Formal statement

section
open Finset

namespace D1Bound5


theorem _root_.D1Bound5.coherent_cpow_half_sub_one_norm_le
    (w : ℂ) (hw : ‖w‖ < 1) :
    ‖((1 + w) ^ (1 / 2 : ℂ)) - 1‖ ≤
      (1 / 2 : ℝ) * ‖w‖ / (1 - ‖w‖) := by sorry



end D1Bound5
end

Source

D1Bound5/CoherentNearOne.lean, lines 7-46, SHA-256 2bc9cb36fbc13ebd4a45c12aad522c318dab7df9ff1f0b30190b7ecf486f48dd. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph