Documentation

Lean 4 Proof

theorem curvature_conservation (_hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) (_hρne : ρ ≠ 0)
    {c w : ℝ} (hc : 0 < c) (hw : 0 < w) :
    |cesEigenvaluePerp J ρ c| * |dualEigenvaluePerp J ρ w| =
    1 / (↑J * c * w) := by
  simp only [cesEigenvaluePerp, dualEigenvaluePerp]
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (by omega : 0 < J)
  have hρ1 : (0 : ℝ) < 1 - ρ := by linarith
  have h1ρne : (1 : ℝ) - ρ ≠ 0 := ne_of_gt hρ1
  rw [show -(1 - ρ) / (↑J * c) = -((1 - ρ) / (↑J * c)) from by ring]
  rw [show -(1 / (1 - ρ)) / w = -((1 / (1 - ρ)) / w) from by ring]
  rw [abs_neg, abs_neg]
  rw [abs_of_pos (div_pos hρ1 (mul_pos hJpos hc))]
  rw [abs_of_pos (div_pos (div_pos one_pos hρ1) hw)]
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:125

Module Section

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

In the same file