Documentation

Lean 4 Proof

theorem trade_weighted_response_bounded {N : ℕ}
    {w response : Fin N → ℝ}
    (hw_nn : ∀ j, 0 ≤ w j)
    (hw_sum : ∑ j : Fin N, w j = 1)
    {r_max : ℝ} (hr : ∀ j, response j ≤ r_max) :
    tradeWeightedResponse N w response ≤ r_max := by
  simp only [tradeWeightedResponse]
  calc ∑ j : Fin N, w j * response j
      ≤ ∑ j : Fin N, w j * r_max := by
        apply Finset.sum_le_sum
        intro j _
        exact mul_le_mul_of_nonneg_left (hr j) (hw_nn j)
    _ = (∑ j : Fin N, w j) * r_max := by rw [Finset.sum_mul]
    _ = 1 * r_max := by rw [hw_sum]
    _ = r_max := one_mul _

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:161

Module Section

Open Economy Monetary Transmission

In the same file