Den Pos

lemma proved Info Geometry

Lean 4 Proof

private lemma den_pos {r : ℝ} {J : ℕ} (hJ : 2 ≤ J) (hr : 0 ≤ r) :
    (0 : ℝ) < 1 + (↑J - 1) * r := by
  have := hJ_sub_one_pos hJ
  positivity

Dependency Graph

Used by

gap_from_one_nonneg correlation_le_one correlation_above_floor correlation_floor_identity gap_from_one

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:81

Module Section

Correlation Convergence at the Regime Boundary

In the same file

compoundSymmetryCorr compoundSymmetryCorr_zero compoundSymmetryCorr_one hJ_sub_one_pos gap_from_one correlation_floor_identity correlation_above_floor correlation_le_one gap_from_one_le gap_from_one_nonneg price_convergence_linear quantity_correlation_to_floor crisis_correlation_dual