IndisputableMonolith.NumberTheory.XiJBridge

declarations in this module (18)

• theorem jcost_exp_eq_cosh L41
• def xiMap L49
• theorem xiMap_pos L51
• theorem xiMap_ne_zero L53
• theorem xiMap_at_half L56
• theorem xiMap_reflection L61
• theorem xiMap_strictMono L67
• theorem xiMap_eq_exp_zeroDeviation L75
• theorem jcost_xiMap_eq_cosh L83
• theorem jcost_xiMap_at_half L88
• theorem jcost_xiMap_nonneg L92
• theorem jcost_xiMap_functional_symmetry L97
• theorem rh_equivalent_to_zero_cost L102
• theorem rcl_defect_coordinates L120
• theorem xiMap_mul_reflection L133
• theorem xiMap_div_reflection L138
• theorem paired_zero_composition L156
• theorem self_composition_cosh L170