def definition def or abbrev

`c_T_squared`

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

formal statement (Lean)

  11noncomputable def c_T_squared (α C_lag : ℝ) : ℝ :=

Definition body.

  12  1 + 0.01 * (α * C_lag)
  13

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

coupling_bound_from_GW170817_hypothesis in IndisputableMonolith.Relativity.GW.Constraints decl_use
c_T_squared_derived in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use
c_T_squared_GR_limit in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use
c_T_squared_near_one in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use
c_T_squared_RS in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use

Lean names referenced from this declaration's body.