Shared quadratic bound and vector L² triangle inequality.

theorem AVenhance.Infra.VectorL2Triangle.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

A nonnegative quadratic bounds its cross coefficient.

theorem AVenhance.Infra.VectorL2Triangle.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 triangle inequality for the coordinate-vector carrier.