Dual Eigenvalue Perp

def proved Foundations

Documentation

Lean 4 Proof

def dualEigenvaluePerp (_J : ℕ) (ρ w : ℝ) : ℝ :=
  -(1 / (1 - ρ)) / w

Dependency Graph

Used by

curvature_conservation weighted_conservation_at_equal_weights curvature_conservation_as_holder_complement

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:114

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file

cesThirdDerivValue ces_third_derivative_pos asymmetryRatio asymmetry_exceeds_one knockoutRetained knockout_partial_retained knockout_total_failure knockout_no_failure criticalFailures dualExponent curvature_conservation excessSavingCoeff substitution_savings