  18  vbul  : ℝ → ℝ
  19
  20/-! Configurable numeric regularization parameters. -/
  21structure Config where
  22  upsilonStar : ℝ
  23  eps_r : ℝ
  24  eps_v : ℝ
  25  eps_t : ℝ
  26  eps_a : ℝ
  27
  28@[simp] def defaultConfig : Config :=
  29  { upsilonStar := 1.0
  30  , eps_r := 1e-12
  31  , eps_v := 1e-12
  32  , eps_t := 0.01
  33  , eps_a := 1e-12 }
  34
  35structure ConfigProps (cfg : Config) : Prop where
  36  eps_t_nonneg : 0 ≤ cfg.eps_t
  37  eps_t_le_one : cfg.eps_t ≤ 1
  38
  39@[simp] lemma defaultConfig_props : ConfigProps defaultConfig := by
  40  refine ⟨?h0, ?h1⟩ <;> norm_num
  41
  42def vbarSq_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
  43  max 0 ((C.vgas r) ^ 2 + ((Real.sqrt cfg.upsilonStar) * (C.vdisk r)) ^ 2 + (C.vbul r) ^ 2)
  44
  45def vbar_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
  46  Real.sqrt (max cfg.eps_v (vbarSq_with cfg C r))
  47
  48def gbar_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
  49  (vbar_with cfg C r) ^ 2 / max cfg.eps_r r
  50
  51structure Params where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.