Euclidean bridge for the HTilde_m gradient

The Hmr gradient estimates are eLpNorms of Vec 2-valued maps, measured with the ambient Pi sup norm. The spaceTimeGradNormSq integrates vecNormSq (the Euclidean norm squared). In dimension two, vecNormSq v ≤ 2 ‖v‖², which costs the factor √2.

theorem AVenhance.Infra.Section5.RelativeError.vecNormSq_two_le (v : Homogenization.Vec 2) : Homogenization.vecNormSq v ≤ 2 * ‖v‖ ^ 2

In dimension two the Euclidean norm squared is at most twice the sup norm squared.

theorem AVenhance.Infra.Section5.RelativeError.ofReal_vecNormSq_le (v : Homogenization.Vec 2) : ENNReal.ofReal (Homogenization.vecNormSq v) ≤ 2 * ‖v‖ₑ ^ 2

Pointwise ENNReal form of vecNormSq_two_le.

theorem AVenhance.Infra.Section5.RelativeError.integral_vecNormSq_le_of_eLpNorm_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (g : α → Homogenization.Vec 2) {B : ℝ} (hB : 0 ≤ B) (h : MeasureTheory.eLpNorm g 2 μ ≤ ENNReal.ofReal B) : ∫ (z : α), Homogenization.vecNormSq (g z) ∂μ ≤ 2 * B ^ 2

The Euclidean integral of a vector field with sup-norm L² bound B is at most 2 B².

theorem AVenhance.Infra.Section5.RelativeError.sqrt_integral_vecNormSq_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (g : α → Homogenization.Vec 2) {B : ℝ} (hB : 0 ≤ B) (h : MeasureTheory.eLpNorm g 2 μ ≤ ENNReal.ofReal B) : √(∫ (z : α), Homogenization.vecNormSq (g z) ∂μ) ≤ √2 * B

Euclidean √∫|g|² is at most √2 times the sup-norm L² bound.

theorem AVenhance.Infra.Section5.RelativeError.sqrt_spaceTimeGradNormSq_le_of_eLpNorm_le (Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {B : ℝ} (hB : 0 ≤ B) (h : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => Dθ z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal B) : √(spaceTimeGradNormSq Dθ) ≤ √2 * B

The spaceTimeGradNormSq version over the open time cell.