`BookProof.ScalaronFock.fockSmoothPotential_esa` (W : ∀ n, E n → ℝ) (hW : ∀ n, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (W n)) : EssentiallySelfAdjointOn (nestedCore E) (fockSmoothPotent

Initializing...

`BookProof.ScalaronFock.fockSmoothPotential_esa` (W : ∀ n, E n → ℝ) (hW : ∀ n, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (W n)) : EssentiallySelfAdjointOn (nestedCore E) (fockSmoothPotent · Prove2Me