Documentation

Lean 4 Proof

noncomputable def expectedKnockoutLoss
    (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, a j * weightedKnockoutLoss J ρ a j

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:280

Module Section

## General-Weight and IRS Effective Curvature Definitions

In the same file