The finite canonical jet envelope preserves L2 control.

theorem AVenhance.Infra.Section4.amnr_normalized_abs_L2_le {μ : MeasureTheory.Measure AmnrSpace} {f : AmnrSpace → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {W G : ℝ} (hW : 0 < W) (hbound : MeasureTheory.eLpNorm f 2 μ ≤ ENNReal.ofReal (G * W)) : MeasureTheory.eLpNorm (fun (z : AmnrSpace) => |f z| / W) 2 μ ≤ ENNReal.ofReal G

Normalizing an actual measurable scalar jet cancels its positive weight.