The Lean 4 theorem `cutoff_energy_core` in the `ChapterSchrodingerCutoffEsa` chapter of the timepiece formalization

-- Generated from ChapterSchrodingerCutoffEsa.lean — theorem BookProof.SchrodingerCutoff.cutoff_energy_core
import Mathlib
import Definitions.Def_ChapterSchrodingerCutoffEsa
import Definitions.Def_ChapterParityChirality
open BookProof.ChapterParityChirality
open BookProof.SchrodingerCutoff



open MeasureTheory Filter Complex

theorem BookProof.SchrodingerCutoff.cutoff_energy_core
    (V : ℝ → ℝ) (hV : Continuous V) (z : ℂ)
    (u u' u'' : ℝ → ℂ)
    (h1 : ∀ x, HasDerivAt u (u' x) x)
    (h2 : ∀ x, HasDerivAt u' (u'' x) x)
    (heq : ∀ x, -u'' x + (V x : ℂ) * u x = z * u x)
    (hVz : ∀ x, 0 ≤ V x - z.re)
    (hL2 : Integrable fun x => ‖u x‖ ^ 2)
    {C : ℝ} (hC : ∀ y, |deriv chi y| ≤ C)
    {R : ℝ} (hR : 0 < R) :
    (∫ x in Set.Icc (-R) R, (V x - z.re) * ‖u x‖ ^ 2)
        ≤ 2 * C ^ 2 / R ^ 2 * (∫ x, ‖u x‖ ^ 2) ∧
      (∫ x in Set.Icc (-R) R, ‖u' x‖ ^ 2) ≤ 4 * C ^ 2 / R ^ 2 * (∫ x, ‖u x‖ ^ 2) := by sorry