Sections / Section 2: CES Emergence Theorems / modeRate

Mode Rate

noncomputable defprovedFoundations

Documentation

Lean 4 Proof

noncomputable def modeRate (k m : ℕ) : ℝ :=
  if m ≤ 2 then 1
  else (↑k : ℝ) ^ (-(↑(m - 2) : ℝ) / 2)

Dependency Graph

Used by

mode_geometric_decay modeRate_eq_rpow_neg_scaling ces_mode_preserved contraction_rate_bounded non_ces_decays_relative_to_rho convergence_rate_cubic rho_mode_rate_is_one modeRate_in_unit_interval modeAfterL stability_mode_contraction modeRate_lt_one modeRate_pos rg_stability_summary

Location

thesis/CESProofs/Foundations/Emergence.lean:119

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file

aggregationOp IsAggFixedPoint aggregation_fixed_point powerMean_zero powerMean_isFixedPoint modeAfterL ces_mode_preserved mode_geometric_decay modeRate_pos modeRate_lt_one modeRate_in_unit_interval stability_contraction stability_rho_preserved stability_mode_contraction anova_mode_connection sum_sq_ge_inv_card collision_entropy_le_log_J power_sum_bound_concave power_sum_bound_convex power_sum_pos