def definition def or abbrev

`dot`

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

formal statement (Lean)

  21def dot {n : ℕ} (α t : Vec n) : ℝ := ∑ i : Fin n, α i * t i

proof body

Definition body.

  22
  23/-- Componentwise logarithm. -/

used by (40)

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

compensatory_nonneg_of_sqNorm_le_one in IndisputableMonolith.Cost.Ndim.Bridge decl_use
dot_sq_le_sqNorm_mul in IndisputableMonolith.Cost.Ndim.Bridge decl_use
multiplicative_le_additive_of_sqNorm_le_one in IndisputableMonolith.Cost.Ndim.Bridge decl_use
multiplicativeQuadratic in IndisputableMonolith.Cost.Ndim.Bridge decl_use
sqNorm in IndisputableMonolith.Cost.Ndim.Calibration decl_use
sqNorm_uniform in IndisputableMonolith.Cost.Ndim.Calibration decl_use
uniform_sqNorm_one in IndisputableMonolith.Cost.Ndim.Calibration decl_use
aggregate in IndisputableMonolith.Cost.Ndim.Core decl_use
dot_log_hadamardDiv in IndisputableMonolith.Cost.Ndim.Core decl_use
dot_log_hadamardInv in IndisputableMonolith.Cost.Ndim.Core decl_use
dot_log_hadamardMul in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_eq_cosh_logsum in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_eq_zero_iff in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_unit in IndisputableMonolith.Cost.Ndim.Core decl_use
JlogN in IndisputableMonolith.Cost.Ndim.Core decl_use
JlogN_eq_cosh_sub_one in IndisputableMonolith.Cost.Ndim.Core decl_use
Vec in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_dAlembert in IndisputableMonolith.Cost.Ndim.DAlembert decl_use
applyHessian_eq_direction in IndisputableMonolith.Cost.Ndim.Hessian decl_use
applyHessian_of_dot_zero in IndisputableMonolith.Cost.Ndim.Hessian decl_use
gradientEntry in IndisputableMonolith.Cost.Ndim.Hessian decl_use
hessianAt_factor in IndisputableMonolith.Cost.Ndim.Hessian decl_use
hessianEntry in IndisputableMonolith.Cost.Ndim.Hessian decl_use
hessianEntry_zero in IndisputableMonolith.Cost.Ndim.Hessian decl_use
quadraticHessian in IndisputableMonolith.Cost.Ndim.Hessian decl_use
quadraticHessian_eq in IndisputableMonolith.Cost.Ndim.Hessian decl_use
metricEntry_zero in IndisputableMonolith.Cost.Ndim.Metric decl_use
aggregate_eq_one_iff in IndisputableMonolith.Cost.Ndim.Neutrality decl_use
zero_cost_iff_dot_zero in IndisputableMonolith.Cost.Ndim.Neutrality decl_use
AApply in IndisputableMonolith.Cost.Ndim.Projector decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

Vec in IndisputableMonolith.Cost.Ndim.Core decl_use