Documentation

Lean 4 Proof

theorem variance_targeting_improves {sigma_prev delta beta_n m_actual m_floor : ℝ}
    (hs_prev : 0 < sigma_prev) (hd : delta ≠ 0) (hb : 0 < beta_n)
    (hma : 0 < m_actual) (hmf : 0 < m_floor)
    (hexcess : m_actual < m_floor) :
    effectiveWelfareContribution sigma_prev delta beta_n m_floor <
    effectiveWelfareContribution sigma_prev delta beta_n m_actual :=
  eff_welfare_decreasing_margin hs_prev hd hb hma hmf hexcess

Dependency Graph

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:132

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file