The Lean 4 theorem `ell2ShiftInvert_le_one` in the `ChapterHashimotoShiftInvert` chapter of the timepiece formalization

Proved

BookProof.HashimotoShiftInvert.ell2ShiftInvert_le_one

by leonardopedro · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem ell2ShiftInvert_le_one in the ChapterHashimotoShiftInvert chapter of the timepiece formalization.

Preamble

-- Generated from ChapterHashimotoShiftInvert.lean — theorem BookProof.HashimotoShiftInvert.ell2ShiftInvert_le_one
import Mathlib
import Definitions.Def_ChapterHashimotoShiftInvert
open BookProof.HashimotoShiftInvert
open scoped lp



open BookProof.FarisLavine BookProof.YangMillsFriedrichs BookProof.YangMillsFriedrichsLimit
open scoped lp
open BookProof.HermiteGalerkin
open scoped lp
open Filter Topology
open scoped lp

Formal statement

theorem BookProof.HashimotoShiftInvert.ell2ShiftInvert_le_one (v : ℓ²(ℕ, ℂ)) :
    (1 : ℝ) * ‖ell2ShiftInvert v‖ ^ 2 ≤ (inner ℂ (ell2ShiftInvert v) v : ℂ).re := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterHashimotoShiftInvert.lean

View graph