Vector L2 triangle inequality with a narrow analysis import.

theorem AVenhance.Infra.Section5.RelativeError.RelativeVectorTriangle.quadratic_cross_bound {A B R : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hp : ∀ (t : ℝ), 0 ≤ t ^ 2 * A - 2 * t * R + B) : R ≤ √A * √B

theorem AVenhance.Infra.Section5.RelativeError.relative_vector_integral_L2_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → Homogenization.Vec 2} (hf : MeasureTheory.Integrable (fun (x : α) => Homogenization.vecNormSq (f x)) μ) (hg : MeasureTheory.Integrable (fun (x : α) => Homogenization.vecNormSq (g x)) μ) (hfg : MeasureTheory.Integrable (fun (x : α) => Homogenization.vecDot (f x) (g x)) μ) : √(∫ (x : α), Homogenization.vecNormSq (f x + g x) ∂μ) ≤ √(∫ (x : α), Homogenization.vecNormSq (f x) ∂μ) + √(∫ (x : α), Homogenization.vecNormSq (g x) ∂μ)

The integral L2 triangle inequality for the actual Vec 2 carrier.