Cost.Ndim.Bridge
IndisputableMonolith.Cost.Ndim.Bridge
No prose has been written for this declaration yet. The Lean source and graph data below render without it.
generate prose now
Lean names referenced from this declaration's body.
IndisputableMonolith.Cost.Ndim.Core
additiveQuadratic
multiplicativeQuadratic
compensatoryQuadratic
additive_decomposition
dot_sq_le_sqNorm_mul
multiplicative_le_additive_of_sqNorm_le_one
compensatory_nonneg_of_sqNorm_le_one