H J Sub One Pos

lemma proved Info Geometry

Lean 4 Proof

private lemma hJ_sub_one_pos {J : ℕ} (hJ : 2 ≤ J) : (0 : ℝ) < ↑J - 1 := by
  have : (2 : ℝ) ≤ ↑J := Nat.ofNat_le_cast.mpr hJ; linarith

Dependency Graph

Used by

gap_from_one_nonneg correlation_le_one den_pos correlation_above_floor correlation_floor_identity gap_from_one_le

Location

thesis/CESProofs/Foundations/CorrelationConvergence.lean:78

Module Section

Correlation Convergence at the Regime Boundary

In the same file

compoundSymmetryCorr compoundSymmetryCorr_zero compoundSymmetryCorr_one den_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