theorem l1Norm_le_sqrt_card_mul_l2Norm {α : Type u_1} [Fintype α] {𝕜 : Type u_3} [RCLike 𝕜] (a : α → 𝕜) : ‖a‖_[1] ≤ √↑(Fintype.card α) * ‖a‖_[2]

theorem lpNorm_eq_card_rpow_mul_nlpNorm {α : Type u_1} [Fintype α] {𝕜 : Type u_3} [RCLike 𝕜] (a : α → 𝕜) (p : NNReal) (hp : p ≠ 0) : ‖a‖_[↑p] = ↑(Fintype.card α) ^ (↑p)⁻¹ * ‖a‖ₙ_[↑p]

theorem lpNorm_le_card_rpow_mul_linftyNorm {α : Type u_1} [Fintype α] {𝕜 : Type u_3} [RCLike 𝕜] (a : α → 𝕜) (p : NNReal) (hp : p ≠ 0) : ‖a‖_[↑p] ≤ ↑(Fintype.card α) ^ (↑p)⁻¹ * ‖a‖_[⊤]

theorem l2Inner_le_l1Norm_mul_linftyNorm {α : Type u_1} [Fintype α] {𝕜 : Type u_3} [RCLike 𝕜] (a : α → 𝕜) (b : α → 𝕜) : ‖l2Inner a b‖ ≤ ‖a‖_[1] * ‖b‖_[⊤]

theorem l2Norm_le_sqrt_l1Norm_mul_linftyNorm {α : Type u_1} [Fintype α] (a : α → ℝ) : ‖a‖_[2] ≤ √(‖a‖_[1] * ‖a‖_[⊤])