lemma
proved
sumFirst_nonneg
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Streams on GitHub at line 107.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
104 have hmod : (i.val % 8) = i.val := Nat.mod_eq_of_lt i.isLt
105 simp [hmod]
106
107lemma sumFirst_nonneg (m : Nat) (s : Stream) : 0 ≤ sumFirst m s := by
108 unfold sumFirst
109 apply Finset.sum_nonneg
110 intro i _
111 split
112 · norm_num
113 · norm_num
114
115lemma sumFirst_eq_zero_of_all_false {m : Nat} {s : Stream}
116 (h : ∀ i : Fin m, s i.val = false) :
117 sumFirst m s = 0 := by
118 unfold sumFirst
119 have : (fun i : Fin m => (if s i.val then 1 else 0)) = (fun _ => 0) := by
120 funext i; simp [h i]
121 simp [this]
122
123end Streams
124
125end IndisputableMonolith