Documentation

Lean 4 Proof

theorem substitution_savings (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) :
    excessSavingCoeff J ρ = (↑J - 1) / (2 * ↑J ^ 2 * (1 - ρ)) := by
  simp only [excessSavingCoeff, curvatureK]
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (by omega : 0 < J)
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  have hJ1 : (0 : ℝ) < ↑J - 1 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
    linarith
  have hJ1ne : (↑J : ℝ) - 1 ≠ 0 := ne_of_gt hJ1
  have hρ1 : (0 : ℝ) < 1 - ρ := by linarith
  have hρ1ne : (1 : ℝ) - ρ ≠ 0 := ne_of_gt hρ1
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:156

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file