Documentation

Lean 4 Proof

theorem activation_threshold_with_weights
    {N : ℕ} (e : WeightedHierarchicalCESEconomy N)
    (hN : 0 < N) :
    1 < (weightedCycleProductBeta e) ^ ((1 : ℝ) / ↑N)
    ↔ 1 < weightedCycleProductBeta e := by
  unfold weightedCycleProductBeta
  exact activation_threshold_iff_product
    (cycleProductBeta_pos e.toHierarchicalCESEconomy) hN

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Activation.lean:192

Module Section

## Activation with Weights and IRS

In the same file