Documentation

Lean 4 Proof

theorem K_reduction_equal_weights (hJ : 0 < J) {ρ : ℝ} :
    generalCurvatureK J ρ (fun _ : Fin J => (1 / ↑J : ℝ)) = curvatureK J ρ := by
  simp only [generalCurvatureK, curvatureK, herfindahlIndex]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/GeneralWeights.lean:102

Module Section

General-weight CES results (Paper 1, Section 10):

In the same file