Quadratic upper

theorem quadratic_upper :    ∀ᵐ x ∂(MeasureTheory.volume.restrict Ω), ∀ ξ : AmbientSpace d,      ⟪ξ, matMulE (A.a x) ξ⟫_ℝ ≤ A.Λ * ‖ξ‖ ^ 2 := by  filter_upwards [A.coercive, A.mulVec_sq_le] with x hx_coercive hx_mul ξ  let q : ℝ := ⟪ξ, matMulE (A.a x) ξ⟫_ℝ  let m : ℝ := ‖matMulE (A.a x) ξ‖  let n : ℝ := ‖ξ‖  have hq_nonneg : 0 ≤ q := by    exact le_trans (mul_nonneg A.lam_nonneg (sq_nonneg ‖ξ‖)) (by simpa [q] using hx_coercive ξ)  have hq_le : q ≤ n * m := by    simpa [q, m, n, abs_of_nonneg hq_nonneg, mul_comm] using      (abs_real_inner_le_norm ξ (matMulE (A.a x) ξ))  have hm_sq : m ^ 2 ≤ A.Λ * q := by    simpa [m, q] using hx_mul ξ  have hn_nonneg : 0 ≤ n := norm_nonneg ξ  have hm_nonneg : 0 ≤ m := norm_nonneg (matMulE (A.a x) ξ)  have hq_mul : q * q ≤ (A.Λ * n ^ 2) * q := by    nlinarith [hq_le, hm_sq, hn_nonneg, hm_nonneg, A.Λ_nonneg]  have hupper : q ≤ A.Λ * n ^ 2 := by    by_cases hq_zero : q = 0    · have hnonneg : 0 ≤ A.Λ * n ^ 2 := mul_nonneg A.Λ_nonneg (sq_nonneg n)      simpa [hq_zero] using hnonneg    · have hq_pos : 0 < q := lt_of_le_of_ne hq_nonneg (by simpa [eq_comm] using hq_zero)      exact le_of_mul_le_mul_right        (by simpa [pow_two, mul_assoc, mul_left_comm, mul_comm] using hq_mul)        hq_pos  simpa [q, n] using hupper