Documentation

Lean 4 Proof

theorem variance_implies_margin_floor {sigma0_sq T Tstar V_target : ℝ}
    (_hs : 0 < sigma0_sq) (hTs : 0 < Tstar) (hTlt : T < Tstar)
    (hV : 0 < V_target)
    (hvar : varianceAtFriction sigma0_sq T Tstar ≤ V_target) :
    marginFloor sigma0_sq V_target ≤ 1 - T / Tstar := by
  simp only [marginFloor, varianceAtFriction] at *
  have hm : 0 < 1 - T / Tstar := by
    rw [sub_pos, div_lt_one hTs]; exact hTlt
  rw [div_le_iff₀ hV]
  rw [div_le_iff₀ hm] at hvar
  linarith [mul_comm V_target (1 - T / Tstar)]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:62

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file