`BookProof.LimitCircleExample.exists_smooth_potential_not_essentiallySelfAdjoint` : ∃ (V : ℝ → ℝ) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V), ¬ EssentiallySelfAdjointOn (ccDomain

Initializing...

`BookProof.LimitCircleExample.exists_smooth_potential_not_essentiallySelfAdjoint` : ∃ (V : ℝ → ℝ) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V), ¬ EssentiallySelfAdjointOn (ccDomain · Prove2Me