gbar_with

formal source

  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
  52  alpha      : ℝ
  53  Clag       : ℝ
  54  A          : ℝ
  55  r0         : ℝ
  56  p          : ℝ
  57  hz_over_Rd : ℝ
  58
  59structure ParamProps (P : Params) : Prop where
  60  alpha_nonneg : 0 ≤ P.alpha
  61  Clag_nonneg  : 0 ≤ P.Clag
  62  Clag_le_one  : P.Clag ≤ 1
  63  A_nonneg     : 0 ≤ P.A
  64  r0_pos       : 0 < P.r0
  65  p_pos        : 0 < P.p
  66
  67def w_t_with (cfg : Config) (P : Params) (Tdyn τ0 : ℝ) : ℝ :=
  68  let t := max cfg.eps_t (Tdyn / τ0)
  69  1 + P.Clag * (Real.rpow t P.alpha - 1)
  70
  71@[simp] def w_t (P : Params) (Tdyn τ0 : ℝ) : ℝ := w_t_with defaultConfig P Tdyn τ0
  72
  73@[simp] def w_t_display (P : Params) (B : BridgeData) (Tdyn : ℝ) : ℝ :=
  74  w_t_with defaultConfig P Tdyn B.tau0
  75
  76lemma eps_t_le_one_default : defaultConfig.eps_t ≤ (1 : ℝ) := by
  77  norm_num
  78