ParamProps

formal source

  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
  79/-- Reference identity under nonzero tick: w_t(τ0, τ0) = 1. -/
  80lemma w_t_ref_with (cfg : Config) (hcfg : ConfigProps cfg)
  81  (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t_with cfg P τ0 τ0 = 1 := by
  82  dsimp [w_t_with]
  83  have hdiv : τ0 / τ0 = (1 : ℝ) := by
  84    field_simp [hτ]
  85  have hmax : max cfg.eps_t (τ0 / τ0) = (1 : ℝ) := by
  86    simpa [hdiv, max_eq_right hcfg.eps_t_le_one]
  87  simp [hmax]
  88
  89lemma w_t_ref (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t P τ0 τ0 = 1 :=