Weakest Link Bottleneck

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem weakest_link_bottleneck {k1 k2 : ℝ} (hk1 : 0 < k1) (h : k1 < k2) :
    1 / k2 < 1 / k1 := by
  exact one_div_lt_one_div_of_lt hk1 h

Dependency Graph

Used by

weakest_link_with_weights

Location

thesis/CESProofs/Hierarchy/Activation.lean:167

Module Section

Theorems 5-6, Proposition 3: Next-Generation Matrix and Activation Threshold

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 sensitivity_ratio_bottleneck activation_threshold_with_weights concentration_bottleneck irs_modified_activation cross_level_amplification_with_weights weakest_link_with_weights