Documentation

Lean 4 Proof

theorem price_convergence_linear {a δ : ℝ} {J : ℕ}
    (hJ : 2 ≤ J) (ha : 0 ≤ a) (hδ : 0 ≤ δ) :
    1 - compoundSymmetryCorr (a * δ) J ≤ ↑J * a * δ := by
  have h := gap_from_one_le hJ (mul_nonneg ha hδ)
  linarith [mul_assoc (↑J : ℝ) a δ]

Dependency Graph

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:180

Module Section

Correlation Convergence at the Regime Boundary

In the same file