w_t_rescale

formal source

  96  have : (c * Tdyn) / (c * τ0) = Tdyn / τ0 := by field_simp [hc0]
  97  simp [this]
  98
  99lemma w_t_rescale (P : Params) (c Tdyn τ0 : ℝ) (hc : 0 < c) :
 100  w_t P (c * Tdyn) (c * τ0) = w_t P Tdyn τ0 :=
 101  w_t_rescale_with defaultConfig P c Tdyn τ0 hc
 102
 103/-- Nonnegativity of time-kernel under ParamProps. -/
 104lemma w_t_nonneg_with (cfg : Config) (hcfg : ConfigProps cfg)
 105  (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
 106  0 ≤ w_t_with cfg P Tdyn τ0 := by
 107  dsimp [w_t_with]
 108  set t := max cfg.eps_t (Tdyn / τ0) with ht
 109  have ht_nonneg : 0 ≤ t := by
 110    have hle : cfg.eps_t ≤ t := by
 111      simpa [ht] using le_max_left cfg.eps_t (Tdyn / τ0)
 112    exact le_trans hcfg.eps_t_nonneg hle
 113  have hrpow_nonneg : 0 ≤ Real.rpow t P.alpha := by
 114    simpa using Real.rpow_nonneg ht_nonneg P.alpha
 115  have h_rpow_minus_one : (-1 : ℝ) ≤ Real.rpow t P.alpha - 1 := by
 116    linarith
 117  have h_mul : (-P.Clag : ℝ) ≤ P.Clag * (Real.rpow t P.alpha - 1) := by
 118    have h := mul_le_mul_of_nonneg_left h_rpow_minus_one H.Clag_nonneg
 119    -- h : P.Clag * (-1) ≤ P.Clag * (Real.rpow t P.alpha - 1)
 120    simpa using h
 121  have h_base : 0 ≤ (1 : ℝ) - P.Clag := sub_nonneg.mpr H.Clag_le_one
 122  have h_lower : (1 : ℝ) - P.Clag ≤ 1 + P.Clag * (Real.rpow t P.alpha - 1) := by
 123    linarith
 124  exact le_trans h_base h_lower
 125
 126lemma w_t_nonneg (P : Params) (H : ParamProps P) (Tdyn τ0 : ℝ) :
 127    0 ≤ w_t P Tdyn τ0 := by
 128  -- For defaultConfig, eps_t = 0.01 > 0.
 129  -- Thus t = max(0.01, Tdyn/τ0) > 0.