Integrating a bounded cell weight

A nonnegative weight bounded on a cell multiplies its quadratic energy by at most the same cell constant.

theorem ESS.bu_short_weighted_energy_cell_le (Cell S : Set CKN.Foundation.Parabolic.ParabolicPoint) (hCell : MeasurableSet Cell) (hS : MeasurableSet S) (E W : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (C : ℝ) (hC : 0 ≤ C) (hEInt : MeasureTheory.IntegrableOn E Cell MeasureTheory.volume) (hEWInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W z * E z) (Cell ∩ S) MeasureTheory.volume) (hE0 : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ E z) (hW : ∀ z ∈ Cell ∩ S, 0 ≤ W z ∧ W z ≤ C) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Cell ∩ S, W z * E z ≤ C * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Cell, E z

A bounded nonnegative weight on a measurable part of a cell is controlled by the full cell energy integral (lem:bu-small-time).