Documentation

Lean 4 Proof

theorem marginFloor_antitone {sigma0_sq V1 V2 : ℝ}
    (hs : 0 < sigma0_sq) (hV1 : 0 < V1) (_hV2 : 0 < V2) (h : V1 < V2) :
    marginFloor sigma0_sq V2 < marginFloor sigma0_sq V1 :=
  div_lt_div_of_pos_left hs hV1 h

Dependency Graph

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:47

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file