Documentation

Lean 4 Proof

theorem ols_bias_magnitude (covZε varZ₁ varZ₂ : ℝ)
    (hvar₁ : 0 < varZ₁) (hvar₂ : 0 < varZ₂)
    (hcov : 0 < covZε) (hmore : varZ₁ < varZ₂) :
    |simultaneityBias covZε varZ₂| < |simultaneityBias covZε varZ₁| := by
  simp only [simultaneityBias, abs_div, abs_of_pos hcov,
             abs_of_pos hvar₁, abs_of_pos hvar₂]
  exact div_lt_div_of_pos_left hcov hvar₁ hmore

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:243

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file