Documentation

Lean 4 Proof

theorem fr_hasDerivAt {FR₀ S S_crit α_FR : ℝ}
    (hSc : 0 < S_crit) (_hS_nn : 0 ≤ S) (hS : S < S_crit) :
    HasDerivAt (fun s => FR₀ * (1 - s / S_crit) ^ α_FR)
      (FR₀ * ((-1 / S_crit) * α_FR * (1 - S / S_crit) ^ (α_FR - 1))) S := by
  have h_inner : HasDerivAt (fun s => 1 - s / S_crit) (-1 / S_crit) S := by
    have := (hasDerivAt_id S).div_const S_crit
    exact (hasDerivAt_const S 1).sub this |>.congr_deriv (by ring)
  have h_pos : (1 - S / S_crit) ≠ 0 := by
    have : S / S_crit < 1 := by rwa [div_lt_one hSc]
    linarith
  have h_rpow : HasDerivAt (fun y => (1 - y / S_crit) ^ α_FR)
      ((-1 / S_crit) * α_FR * (1 - S / S_crit) ^ (α_FR - 1)) S :=
    h_inner.rpow_const (p := α_FR) (Or.inl h_pos)
  exact ((hasDerivAt_const S FR₀).mul h_rpow).congr_deriv (by ring)

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:436

Module Section

Paper 7: Settlement Feedback and Monetary Policy in a Mesh Economy

In the same file