Local integrability of the short-time weights

The three density factors are continuous on the high strip, and their cell bounds make their products with locally integrable energy integrable on each cell.

theorem ESS.bu_short_high_strip_subset_positive (scale : ℝ) (hscale : 0 < scale) : buShortHighStrip scale ⊆ {z : CKN.Foundation.Parabolic.ParabolicPoint | 0 < z.1 2 ∧ 0 < z.2}

The high strip has strictly positive height and time.

theorem ESS.bu_short_integrable_mul_bounded_on (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (hS : MeasurableSet S) (E W : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hE : MeasureTheory.IntegrableOn E S MeasureTheory.volume) (hWcont : ContinuousOn W S) (C : ℝ) (hWbound : ∀ z ∈ S, ‖W z‖ ≤ C) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W z * E z) S MeasureTheory.volume

Multiplication by a bounded continuous scalar factor preserves integrability on a measurable cell fragment.