Documentation

Lean 4 Proof

theorem policy_dichotomy {phi_prev sigma1 sigma2 c delta : ℝ}
    {sigma_prev beta_n m1 m2 : ℝ}
    (hs1 : sigma1 ≠ 0) (hs2 : sigma2 ≠ 0)
    (hs_prev : 0 < sigma_prev) (hd : delta ≠ 0) (hb : 0 < beta_n)
    (hm1 : 0 < m1) (hm2 : 0 < m2) (hm : m1 < m2) :
    -- Part (a): σ-channel cancels in welfare
    c * (phi_prev / sigma1) * sigma1 * delta ^ 2 =
    c * (phi_prev / sigma2) * sigma2 * delta ^ 2
    -- Part (b): margin channel is strictly monotone
    ∧ effectiveWelfareContribution sigma_prev delta beta_n m2 <
      effectiveWelfareContribution sigma_prev delta beta_n m1 :=
  ⟨welfare_independent_of_own_sigma hs1 hs2,
   eff_welfare_decreasing_margin hs_prev hd hb hm1 hm2 hm⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:107

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file