Documentation

Lean 4 Proof

theorem cbdc_acceleration_reinforced
    {num_sq num_cbdc denom_sq denom_cbdc : ℝ}
    (hnum_sq : 0 < num_sq)
    (hdenom_sq : 0 < denom_sq) (hdenom_cbdc : 0 < denom_cbdc)
    (h_num : num_sq < num_cbdc)
    (h_denom : denom_cbdc ≤ denom_sq) :
    num_sq / denom_sq < num_cbdc / denom_cbdc := by
  rw [div_lt_div_iff₀ hdenom_sq hdenom_cbdc]
  calc num_sq * denom_cbdc
      ≤ num_sq * denom_sq :=
        mul_le_mul_of_nonneg_left h_denom (le_of_lt hnum_sq)
    _ < num_cbdc * denom_sq :=
        mul_lt_mul_of_pos_right h_num hdenom_sq

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:236

Module Section

Paper 7: Settlement Feedback and Monetary Policy in a Mesh Economy

In the same file