Documentation

Lean 4 Proof

theorem variance_upstream_complement {sigma_prev1 sigma_prev2 delta beta_n m1 m2 : ℝ}
    (_hs1 : 0 < sigma_prev1) (_hs2 : 0 < sigma_prev2)
    (hd : delta ≠ 0) (hb : 0 < beta_n)
    (hm1 : 0 < m1) (_hm2 : 0 < m2)
    (h_sigma : sigma_prev2 < sigma_prev1)
    (h_margin : m1 < m2) :
    effectiveWelfareContribution sigma_prev2 delta beta_n m2 <
    effectiveWelfareContribution sigma_prev1 delta beta_n m1 := by
  simp only [effectiveWelfareContribution]
  have hd2 : 0 < delta ^ 2 := sq_pos_of_ne_zero hd
  have hnum : sigma_prev2 * delta ^ 2 < sigma_prev1 * delta ^ 2 :=
    mul_lt_mul_of_pos_right h_sigma hd2
  have hdenom : beta_n * m1 < beta_n * m2 :=
    mul_lt_mul_of_pos_left h_margin hb
  calc sigma_prev2 * delta ^ 2 / (beta_n * m2)
      < sigma_prev1 * delta ^ 2 / (beta_n * m2) :=
        div_lt_div_of_pos_right hnum (mul_pos hb (by linarith : (0 : ℝ) < m2))
    _ < sigma_prev1 * delta ^ 2 / (beta_n * m1) :=
        div_lt_div_of_pos_left (mul_pos (by linarith : (0 : ℝ) < sigma_prev1) hd2)
          (mul_pos hb hm1) hdenom

Dependency Graph

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:154

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file