theorem proved term proof

`aggregate_pos`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  47@[simp] theorem aggregate_pos {n : ℕ} (α x : Vec n) : 0 < aggregate α x := by

Term-mode proof.

  48  unfold aggregate
  49  exact Real.exp_pos _
  50

From the project-wide theorem graph. These declarations reference this one in their body.

JcostN_nonneg in IndisputableMonolith.Cost.Ndim.Core decl_use
forced_of_scalar_uniqueness in IndisputableMonolith.Cost.Ndim.Uniqueness decl_use
det_xHessianMatrix2_formula in IndisputableMonolith.Cost.Ndim.XCoordinates decl_use
det_xHessianMatrix2_ne_zero_of_generic in IndisputableMonolith.Cost.Ndim.XCoordinates decl_use

Lean names referenced from this declaration's body.