Documentation

Lean 4 Proof

theorem inner_multiplier_monotone {J1 J2 : ℕ} {ρ : ℝ}
    (hρ : 0 < ρ) (hρ1 : ρ < 1) (_hJ1 : 1 ≤ J1) (hJ : J1 ≤ J2) :
    innerDiversityMultiplier J1 ρ ≤ innerDiversityMultiplier J2 ρ := by
  unfold innerDiversityMultiplier
  apply rpow_le_rpow (by positivity) (Nat.cast_le.mpr hJ)
  exact div_nonneg (by linarith) (le_of_lt hρ)

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:313

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file