abbrev definition def or abbrev

`Vec`

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

formal statement (Lean)

  18abbrev Vec (n : ℕ) := Fin n → ℝ

proof body

Definition body.

  19
  20/-- Weighted dot product used by the logarithmic aggregate. -/

used by (40)

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

additive_decomposition in IndisputableMonolith.Cost.Ndim.Bridge decl_use
additiveQuadratic in IndisputableMonolith.Cost.Ndim.Bridge decl_use
compensatory_nonneg_of_sqNorm_le_one in IndisputableMonolith.Cost.Ndim.Bridge decl_use
compensatoryQuadratic 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
uniform_weight_of_sum_one in IndisputableMonolith.Cost.Ndim.Calibration decl_use
UniformWeights in IndisputableMonolith.Cost.Ndim.Calibration decl_use
weightSum in IndisputableMonolith.Cost.Ndim.Calibration decl_use
weightSum_uniform in IndisputableMonolith.Cost.Ndim.Calibration decl_use
not_projectivelyEquivalentToZeroAt_tPulledConnection in IndisputableMonolith.Cost.Ndim.Connections decl_use
projectivelyEquivalent_one_dim in IndisputableMonolith.Cost.Ndim.Connections decl_use
ProjectivelyEquivalentToZeroAt in IndisputableMonolith.Cost.Ndim.Connections decl_use
tPulledConnection in IndisputableMonolith.Cost.Ndim.Connections decl_use
tPulledConnection_diag in IndisputableMonolith.Cost.Ndim.Connections decl_use
tPulledConnection_offDiag in IndisputableMonolith.Cost.Ndim.Connections decl_use
xFlatConnection in IndisputableMonolith.Cost.Ndim.Connections decl_use
xFlatConnection_apply in IndisputableMonolith.Cost.Ndim.Connections decl_use
aggregate in IndisputableMonolith.Cost.Ndim.Core decl_use
aggregate_pos in IndisputableMonolith.Cost.Ndim.Core decl_use
dot 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
hadamardDiv in IndisputableMonolith.Cost.Ndim.Core decl_use
hadamardInv in IndisputableMonolith.Cost.Ndim.Core decl_use

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.

aggregate in IndisputableMonolith.Cost.Ndim.Core decl_use
dot in IndisputableMonolith.Cost.Ndim.Core decl_use