← Mathematical handbook

noncomputable def Verification.extendFin {n : ℕ} (a : Fin n → ℝ) (i : ℕ) : ℝ

Equations

• Verification.extendFin a i = if hi : i < n then a ⟨i, hi⟩ else 0

theorem Verification.sum_extendFin_prefix {n : ℕ} (a : Fin n → ℝ) (k : ℕ) (hk : k ≤ n) : (∑ i : Fin n, if ↑i < k then a i else 0) = ∑ i ∈ Finset.range k, extendFin a i

theorem Verification.majorization_fin_sum_sq {n : ℕ} (a b : Fin n → ℝ) (hb : Antitone b) (hp : ∀ (k : Fin (n + 1)), (∑ i : Fin n, if ↑i < ↑k then b i else 0) ≤ ∑ i : Fin n, if ↑i < ↑k then a i else 0) (ht : ∑ i : Fin n, a i = ∑ i : Fin n, b i) : ∑ i : Fin n, b i ^ 2 ≤ ∑ i : Fin n, a i ^ 2