Sections / Section 2: CES Emergence Theorems / modeAfterL

Mode After L

noncomputable defprovedFoundations

Documentation

Lean 4 Proof

noncomputable def modeAfterL (k m L : ℕ) (a₀ : ℝ) : ℝ :=
  (modeRate k m) ^ L * a₀

Dependency Graph

Used by

basin_of_attraction_structure mode_geometric_decay ces_mode_preserved stability_contraction modeAfterL_eq_rpow_scaling basin_is_global contraction_rate_bounded non_ces_decays_relative_to_rho convergence_rate_cubic anova_mode_connection aggregation_invariance_of_rho stability_rho_preserved

Location

thesis/CESProofs/Foundations/Emergence.lean:125

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file

aggregationOp IsAggFixedPoint aggregation_fixed_point powerMean_zero powerMean_isFixedPoint modeRate 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