Documentation

Lean 4 Proof

theorem hierarchy_approximation_quality (net : ComplementarityNetwork J)
    (P : HierarchicalPartition J N) {ε : ℝ} (_hε : 0 ≤ ε)
    (hnd : isNearDecomposable net P ε) (v : Fin J → ℝ) :
    interLevelQF net P v ≤ ε * crossLevelDistQF P v := by
  unfold interLevelQF crossLevelDistQF
  set A := ∑ j : Fin J, ∑ k : Fin J,
    (if P.level j ≠ P.level k then net.w j k else 0) * (v j - v k) ^ 2
  set B := ∑ j : Fin J, ∑ k : Fin J,
    (if P.level j ≠ P.level k then (1:ℝ) else 0) * (v j - v k) ^ 2
  -- Reduce to pointwise bound on inner sums
  suffices hAB : A ≤ ε * B by
    calc 1 / 2 * A ≤ 1 / 2 * (ε * B) := mul_le_mul_of_nonneg_left hAB (by norm_num)
      _ = ε * (1 / 2 * B) := by ring
  rw [Finset.mul_sum]
  apply Finset.sum_le_sum; intro j _
  rw [Finset.mul_sum]
  apply Finset.sum_le_sum; intro k _
  by_cases h : P.level j ≠ P.level k
  · rw [if_pos h, if_pos h, one_mul]
    exact mul_le_mul_of_nonneg_right (hnd j k h) (sq_nonneg _)
  · push_neg at h; simp [h]

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:316

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file