Documentation

Lean 4 Proof

theorem cointegration_residual_structure (ρ c logShareRatio logFactorRatio : ℝ) :
    logShareRatio - (c + ρ * logFactorRatio) =
    (logShareRatio - c - ρ * logFactorRatio) := by ring

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:377

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file