w_t_display

formal source

  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 :=
  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. -/