w_t_ref

formal source

  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 :=
  90  w_t_ref_with defaultConfig defaultConfig_props P τ0 hτ
  91
  92lemma w_t_rescale_with (cfg : Config) (P : Params) (c Tdyn τ0 : ℝ) (hc : 0 < c) :
  93  w_t_with cfg P (c * Tdyn) (c * τ0) = w_t_with cfg P Tdyn τ0 := by
  94  dsimp [w_t_with]
  95  have hc0 : (c : ℝ) ≠ 0 := ne_of_gt hc
  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)