Documentation

Lean 4 Proof

theorem cross_level_amplification_with_weights
    {N : ℕ} (e : WeightedHierarchicalCESEconomy N)
    (hP : 1 < weightedCycleProductBeta e) :
    ∃ n : Fin N, 1 < e.beta n := by
  unfold weightedCycleProductBeta cycleProductBeta at hP
  exact cross_level_amplification _
    (fun n => e.hbeta n) hP

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Activation.lean:219

Module Section

## Activation with Weights and IRS

In the same file