Documentation

Lean 4 Proof

theorem marginFloor_pos {sigma0_sq V_target : ℝ}
    (hs : 0 < sigma0_sq) (hV : 0 < V_target) :
    0 < marginFloor sigma0_sq V_target :=
  div_pos hs hV

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:39

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file