Documentation

Lean 4 Proof

theorem quadratic_channel_present {ρ : ℝ} (hJ : 2 ≤ J) (hρ : ρ < 1) :
    0 < curvatureK J ρ := curvatureK_pos hJ hρ

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:96

Module Section

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

In the same file