The Lean 4 theorem `densY_sq` in the `ChapterQuantumGravityDensitized` chapter of the timepiece formalization

-- Generated from ChapterQuantumGravityDensitized.lean — theorem BookProof.QuantumGravityDensitized.densY_sq
import Definitions.Def_ChapterFarisLavine
import Mathlib
import Definitions.Def_ChapterQuantumGravityDensitized
open BookProof.QuantumGravityDensitized



open Filter Topology BookProof.FarisLavine

theorem BookProof.QuantumGravityDensitized.densY_sq {e : ℝ} (he : 0 ≤ e) : densY e ^ 2 = e := by sorry