Margin Floor

def proved Hierarchy

Documentation

Lean 4 Proof

def marginFloor (sigma0_sq V_target : ℝ) : ℝ := sigma0_sq / V_target

Dependency Graph

Used by

variance_implies_margin_floor marginFloor_pos variance_target_bounds_welfare marginFloor_antitone

Location

thesis/CESProofs/Hierarchy/VarianceTargeting.lean:30

Module Section

Variance Targeting Escapes Damping Cancellation

In the same file

marginFloor_pos marginFloor_antitone variance_implies_margin_floor variance_target_bounds_welfare policy_dichotomy variance_targeting_improves variance_upstream_complement