Weakest Link With Weights

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem weakest_link_with_weights
    {k₁ k₂ : ℝ} (hk₁ : 0 < k₁) (hk : k₁ < k₂) :
    1 / k₂ < 1 / k₁ := by
  exact weakest_link_bottleneck hk₁ hk

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Activation.lean:228

Module Section

## Activation with Weights and IRS

In the same file

ngm_char_poly_two_level activation_two_level ngm_char_poly_general activation_threshold_iff_product reduced_dynamics cross_level_amplification weakest_link_bottleneck sensitivity_ratio_bottleneck activation_threshold_with_weights concentration_bottleneck irs_modified_activation cross_level_amplification_with_weights