Documentation

Lean 4 Proof

theorem variance_target_bounds_welfare {sigma_prev delta beta_n sigma0_sq V_target : ℝ}
    (hs_prev : 0 < sigma_prev) (hd : delta ≠ 0) (hb : 0 < beta_n)
    (hs0 : 0 < sigma0_sq) (hV : 0 < V_target) :
    0 < effectiveWelfareContribution sigma_prev delta beta_n
        (marginFloor sigma0_sq V_target) := by
  simp only [effectiveWelfareContribution]
  apply div_pos
  · exact mul_pos hs_prev (sq_pos_of_ne_zero hd)
  · exact mul_pos hb (marginFloor_pos hs0 hV)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:85

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file