Scalar coordinate L2 jets extracted from actual vector dissipation.

theorem AVenhance.Infra.Section4.amnr_coordinate_sq_le_vecNormSq (v : Homogenization.Vec 2) (q : Fin 2) : v q ^ 2 ≤ Homogenization.vecNormSq v

theorem AVenhance.Infra.Section4.amnr_coordinate_eLpNorm_two_le_of_dissipation {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : α → Homogenization.Vec 2} (q : Fin 2) (hg : MeasureTheory.AEStronglyMeasurable (fun (z : α) => g z q) μ) (hint : MeasureTheory.Integrable (fun (z : α) => Homogenization.vecNormSq (g z)) μ) {G : ℝ} (hG : 0 ≤ G) (hbound : ∫ (z : α), Homogenization.vecNormSq (g z) ∂μ ≤ G ^ 2) : MeasureTheory.eLpNorm (fun (z : α) => g z q) 2 μ ≤ ENNReal.ofReal G

Each scalar gradient coordinate is paid for by the actual full vector quadratic dissipation, on the same measure.