Documentation

Lean 4 Proof

theorem weighted_conservation_at_equal_weights
    {J : ℕ} (hJ : 2 ≤ J) {ρ c w : ℝ} (hρ : ρ < 1) (hρne : ρ ≠ 0)
    (hc : 0 < c) (hw : 0 < w) :
    |cesEigenvaluePerp J ρ c| * |dualEigenvaluePerp J ρ w| =
    1 / ((J : ℝ) * c * w) := by
  exact curvature_conservation hJ hρ hρne hc hw

Dependency Graph

Location

thesis/CESProofs/Potential/PrimalDual.lean:30

Module Section

## Theorem 2b.3: Weighted Curvature Conservation

In the same file