Documentation

Lean 4 Proof

theorem equal_weight_entry_maximizes_K (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {a : Fin J → ℝ} (ha_pos : ∀ j, 0 < a j) (ha_sum : ∑ j : Fin J, a j = 1) :
    generalCurvatureK J ρ a ≤ curvatureK J ρ :=
  equalWeights_maximize_K hJ hρ ha_pos ha_sum

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:176

Module Section

## Entry with General Weights

In the same file