structure definition def or abbrev

`ScalingModel`

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

formal statement (Lean)

   7structure ScalingModel where
   8  gamma : ℝ
   9  f     : ℝ → ℝ → ℝ
  10  f_hom0 : ∀ {c t1 t2}, 0 < c → f (c * t1) (c * t2) = f t1 t2
  11
  12noncomputable section
  13

used by (2)

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

predicted_ratio in IndisputableMonolith.TruthCore.MRD.Scaling decl_use
predicted_ratio_rescale in IndisputableMonolith.TruthCore.MRD.Scaling decl_use

depends on (3)

Lean names referenced from this declaration's body.

gamma in IndisputableMonolith.Constants.EulerMascheroni decl_use
gamma in IndisputableMonolith.NetworkScience.SmallWorldFromSigma decl_use
gamma in IndisputableMonolith.Relativity.ILG.PPN decl_use