def definition def or abbrev

`xiMap`

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

formal statement (Lean)

  49def xiMap (σ : ℝ) : ℝ := Real.exp (2 * (σ - 1 / 2))

Definition body.

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

jcost_xiMap_at_half in IndisputableMonolith.NumberTheory.XiJBridge decl_use
jcost_xiMap_eq_cosh in IndisputableMonolith.NumberTheory.XiJBridge decl_use
jcost_xiMap_functional_symmetry in IndisputableMonolith.NumberTheory.XiJBridge decl_use
jcost_xiMap_nonneg in IndisputableMonolith.NumberTheory.XiJBridge decl_use
paired_zero_composition in IndisputableMonolith.NumberTheory.XiJBridge decl_use
rcl_defect_coordinates in IndisputableMonolith.NumberTheory.XiJBridge decl_use
rh_equivalent_to_zero_cost in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_at_half in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_div_reflection in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_eq_exp_zeroDeviation in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_mul_reflection in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_ne_zero in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_pos in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_reflection in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_strictMono in IndisputableMonolith.NumberTheory.XiJBridge decl_use