IndisputableMonolith.Cost.Ndim.Core

declarations in this module (20)

• abbrev Vec L18
• def dot L21
• def logVec L24
• def hadamardMul L27
• def hadamardInv L30
• def hadamardDiv L33
• def aggregate L36
• def JlogN L40
• def JcostN L44
• theorem aggregate_pos L47
• theorem JcostN_eq_Jcost_aggregate L51
• theorem JlogN_eq_cosh_sub_one L55
• theorem JcostN_eq_cosh_logsum L59
• theorem JcostN_unit L64
• theorem JcostN_nonneg L69
• theorem dot_log_hadamardMul L74
• theorem dot_log_hadamardDiv L92
• theorem dot_log_hadamardInv L110
• theorem JcostN_reciprocal L127
• theorem JcostN_eq_zero_iff L133