`BookProof.ChapterStoneSeparable.mulSA_position_unbounded` : ¬ ∃ C : ℝ, ∀ x : (mulSA positionField).domain, ‖(mulSA positionField).op x‖ ≤ C * ‖(x : L2Z)‖

Proved

BookProof.ChapterStoneSeparable.mulSA_position_unbounded

by leonardopedro · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterStoneSeparable.

BookProof.ChapterStoneSeparable.mulSA_position_unbounded : ¬ ∃ C : ℝ, ∀ x : (mulSA positionField).domain, ‖(mulSA positionField).op x‖ ≤ C * ‖(x : L2Z)‖

Formalization note: Lean 4 identifier BookProof.ChapterStoneSeparable.mulSA_position_unbounded.

Preamble

-- Generated from ChapterStoneSeparable.lean — theorem BookProof.ChapterStoneSeparable.mulSA_position_unbounded
import Definitions.Def_ChapterSirkTrotterKato
import Definitions.Def_ChapterStoneConverse
import Mathlib
import Definitions.Def_ChapterStoneSeparable
import Definitions.Def_ChapterContinuityUnitaryInfinite
import Definitions.Def_ChapterUnboundedPosition
open BookProof.ChapterContinuityUnitaryInfinite
open BookProof.ChapterUnboundedPosition
open BookProof.ChapterStoneSeparable


open scoped InnerProductSpace
open Filter Topology


open BookProof.ChapterStoneResolvent BookProof.ChapterStoneMeasurable

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [TopologicalSpace.SeparableSpace H]

Formal statement

theorem BookProof.ChapterStoneSeparable.mulSA_position_unbounded :
    ¬ ∃ C : ℝ, ∀ x : (mulSA positionField).domain,
      ‖(mulSA positionField).op x‖ ≤ C * ‖(x : L2Z)‖ := by sorry

View graph