noncomputable def Nat.sum_ft (n m : Nat) (x : Nat → Nat) : Nat

Equations

• n.sum_ft m x = Nat.finite_sum fun (i : ↥(Set.Ico n m)) => x i.val

noncomputable def Nat.prod_ft (n m : Nat) (x : Nat → Nat) : Nat

Equations

• n.prod_ft m x = Nat.finite_prod fun (i : ↥(Set.Ico n m)) => x i.val

theorem Nat.sum_ft_ge {n m : Nat} {x : Nat → Nat} (h : m ≤ n) : n.sum_ft m x = 0

theorem Nat.prod_ft_ge {n m : Nat} {x : Nat → Nat} (h : m ≤ n) : n.prod_ft m x = 1

@[simp]

theorem Nat.sum_ft_succ_right {n m : Nat} (h : n ≤ m) {x : Nat → Nat} : n.sum_ft (m + 1) x = n.sum_ft m x + x m

@[simp]

theorem Nat.prod_ft_succ_right {n m : Nat} (h : n ≤ m) {x : Nat → Nat} : n.prod_ft (m + 1) x = n.prod_ft m x * x m

theorem Nat.sum_ft_split {n m k : Nat} (h : n ≤ k) (h' : k ≤ m) {x : Nat → Nat} : n.sum_ft m x = n.sum_ft k x + k.sum_ft m x

theorem Nat.sum_ft_le_expand_right {n m k : Nat} (h : n ≤ k) (h' : k ≤ m) {x : Nat → Nat} : n.sum_ft k x ≤ n.sum_ft m x

@[simp]

theorem Nat.sum_ft_le_expand_one {n m : Nat} (h : n ≤ m) {x : Nat → Nat} : n.sum_ft m x ≤ n.sum_ft (m + 1) x

theorem Nat.prod_ft_split {n m k : Nat} (h : n ≤ k) (h' : k ≤ m) {x : Nat → Nat} : n.prod_ft m x = n.prod_ft k x * k.prod_ft m x

theorem Nat.sum_ft_find_between {n m l : Nat} {x : Nat → Nat} (h : n ≤ m) (h' : l < n.sum_ft m x) : ∃ (k : Nat), n.sum_ft k x ≤ l ∧ l < n.sum_ft (k + 1) x ∧ k < m

theorem Nat.prod_ft_zero_iff_exists_zero {n m : Nat} {x : Nat → Nat} : n.prod_ft m x = 0 ↔ ∃ (i : Nat), n ≤ i ∧ i < m ∧ x i = 0

theorem Nat.prod_minus_one_even {n : Nat} : 2 ∣ n * (n - 1)

theorem Nat.prod_plus_one_even {n : Nat} : 2 ∣ n * (n + 1)

theorem Nat.sum_ft_id {n : Nat} : Nat.sum_ft 0 n id = n * (n - 1) / 2

theorem FiniteType.cardinality_disj_iUnion_ft {n m : Nat} {α : Type} [Finite α] {a : Nat → Set α} (h : Set.Disjoint fun (x : ↥(Set.Ico n m)) => a x.val) : (Finite.ftype ↥(⋃ i : ↥(Set.Ico n m), a i.val)).cardinality = n.sum_ft m fun (i : Nat) => (Finite.ftype ↥(a i)).cardinality