Documentation

Lean 4 Proof

theorem upstream_reform_beta_weighted
    {sigma_prev delta beta_n₁ beta_n₂ : ℝ}
    (hσ : 0 < sigma_prev) (hδ : delta ≠ 0)
    (hβ₁ : 0 < beta_n₁) (hβ₂ : 0 < beta_n₂) (hβ : beta_n₁ < beta_n₂) :
    welfareContribution sigma_prev delta beta_n₂
    < welfareContribution sigma_prev delta beta_n₁ := by
  exact upstream_reform_beta hσ hδ hβ₁ hβ₂ hβ

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:396

Module Section

## Eigenstructure Bridge and Damping Cancellation with Weights

In the same file