(hκ : ∀ i, 0 ≤ κ i) : EssentiallySelfAdjointOn (lpFiniteModes (Occ d)) ((lpFiniteModes (Occ d)).subtype.comp (∑ i, ((1 : ℂ) / 2) • ((mom κ i).comp (drift κ i) + (drift κ i).comp (mom κ i))))

Initializing...

(hκ : ∀ i, 0 ≤ κ i) : EssentiallySelfAdjointOn (lpFiniteModes (Occ d)) ((lpFiniteModes (Occ d)).subtype.comp (∑ i, ((1 : ℂ) / 2) • ((mom κ i).comp (drift κ i) + (drift κ i).comp (mom κ i)))) · Prove2Me