Documentation

Lean 4 Proof

def detectionThresholdLHS (J : ℕ) (ρ : ℝ) (m : EquicorrModel) : ℝ :=
  curvatureK J ρ * m.γ * (1 - m.r)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:113

Module Section

Correlation robustness of CES (Paper 1, Section 7):

In the same file