Documentation

Lean 4 Proof

theorem crisis_correlation_dual {J : ℕ} (hJ : 2 ≤ J) :
    -- (i) Price limit: r = 0 gives cor = 1
    compoundSymmetryCorr 0 J = 1 ∧
    -- (ii) Quantity floor: cor > -1/(J-1) for all finite r
    (∀ r : ℝ, 0 ≤ r → -1 / (↑J - 1) < compoundSymmetryCorr r J) ∧
    -- (iii) Linear bound: beta = 1
    (∀ r : ℝ, 0 ≤ r → 1 - compoundSymmetryCorr r J ≤ ↑J * r) :=
  ⟨compoundSymmetryCorr_zero J,
   fun _ hr => correlation_above_floor hJ hr,
   fun _ hr => gap_from_one_le hJ hr⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:222

Module Section

Correlation Convergence at the Regime Boundary

In the same file