convexBodySumFun_apply' — Mathlib

English

The function convexBodySumFun can be decomposed into real and complex contributions: convexBodySumFun x = sum_w ||x.1 w|| + 2 * sum_w ||x.2 w||.

Русский

Разложение вклада функций: convexBodySumFun x = сумма по real-площадям ||x.1 w|| + 2 * сумма по complex-площадям ||x.2 w||.

LaTeX

$$\$\\text{convexBodySumFun}(x) = \\sum_w \\|x.1_w\\| + 2 \\sum_w \\|x.2_w\\|\$$$

Lean4

theorem convexBodySumFun_apply' (x : mixedSpace K) : convexBodySumFun x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖ := by
  simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex, Nat.cast_one, one_mul,
    Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _), normAtPlace_apply_of_isComplex (Subtype.prop _),
    Finset.mul_sum]

Похожие утверждения