Mixed bound

theorem mixed_bound :    ∀ᵐ x ∂(MeasureTheory.volume.restrict Ω), ∀ ξ ζ : AmbientSpace d,      |⟪ζ, matMulE (A.a x) ξ⟫_ℝ| ≤ A.Λ * ‖ζ‖ * ‖ξ‖ := by  filter_upwards [A.mulVec_sq_le, A.quadratic_upper] with x hx_mul hx_quad  intro ξ ζ  let m : ℝ := ‖matMulE (A.a x) ξ‖  let nξ : ℝ := ‖ξ‖  let nζ : ℝ := ‖ζ‖  have habs : |⟪ζ, matMulE (A.a x) ξ⟫_ℝ| ≤ nζ * m := by    simpa [m, nζ, mul_comm] using abs_real_inner_le_norm ζ (matMulE (A.a x) ξ)  have hm_sq : m ^ 2 ≤ A.Λ * ⟪ξ, matMulE (A.a x) ξ⟫_ℝ := by    simpa [m] using hx_mul ξ  have hq_upper :      ⟪ξ, matMulE (A.a x) ξ⟫_ℝ ≤ A.Λ * nξ ^ 2 := by    simpa [nξ] using hx_quad ξ  have hm_le : m ≤ A.Λ * nξ := by    have hm_nonneg : 0 ≤ m := norm_nonneg (matMulE (A.a x) ξ)    have hnξ_nonneg : 0 ≤ nξ := norm_nonneg ξ    have hrhs_nonneg : 0 ≤ A.Λ * nξ := mul_nonneg A.Λ_nonneg hnξ_nonneg    have hm_sq_upper : m ^ 2 ≤ (A.Λ * nξ) ^ 2 := by      nlinarith [hm_sq, hq_upper, A.Λ_nonneg]    exact (sq_le_sq₀ hm_nonneg hrhs_nonneg).1 hm_sq_upper  have hnζ_nonneg : 0 ≤ nζ := norm_nonneg ζ  calc    |⟪ζ, matMulE (A.a x) ξ⟫_ℝ| ≤ nζ * m := habs    _ ≤ nζ * (A.Λ * nξ) := by      exact mul_le_mul_of_nonneg_left hm_le hnζ_nonneg    _ = A.Λ * ‖ζ‖ * ‖ξ‖ := by      ring