initial commit

src/data/sign.lean

@@ -3,8 +3,7 @@ Copyright (c) 2022 Eric Rodriguez. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
-import order.basic
-import algebra.algebra.basic
+import algebra.big_operators.basic
 import tactic.derive_fintype
 
 /-!
@@ -202,3 +201,58 @@ def sign_hom : α →*₀ sign_type :=
                mul_neg_of_pos_of_neg, mul_pos] }
 
 end linear_ordered_ring
+
+namespace int
+
+@[simp] lemma sign_eq_sign (n : ℤ) : n.sign = _root_.sign n :=
+begin
+  obtain ((_ | _) | _) := n,
+  { exact congr_arg coe sign_zero.symm },
+  { exact congr_arg coe (sign_pos $ int.succ_coe_nat_pos _).symm },
+  { exact congr_arg coe (_root_.sign_neg $ neg_succ_lt_zero _).symm }
+end
+end int
+
+open finset nat
+open_locale big_operators
+
+variables [decidable_eq α] [nonempty α]
+
+-- TODO: Inlining this yields an app-builder exception
+lemma exists_signed_sum_aux {n : ℕ} (sgn : ℕ → sign_type) (b : α) [decidable_eq α] {f : α → ℤ}
+  ⦃a : α⦄ (g : ℕ → α) (i : ℕ) :
+   ite ((range (n - (f a).nat_abs)).piecewise g (λ _, a) i = b)
+        ((range (n - (f a).nat_abs)).piecewise sgn (λ _, sign (f a)) i : ℤ) 0 =
+    (range (n - (f a).nat_abs)).piecewise (λ j, ite (g j = b) ↑(sgn j) 0)
+        (λ j, ite (a = b) ↑(sign (f a)) 0) i :=
+by { unfold piecewise, split_ifs; refl }
+
+lemma exists_signed_sum (s : finset α) (n : ℕ) (f : α → ℤ) (hn : ∑ i in s, (f i).nat_abs ≤ n) :
+  ∃ (sgn : ℕ → sign_type) (g : ℕ → α), (∀ i, g i ∉ s → sgn i = 0) ∧
+    ∀ a ∈ s, (∑ i in range n, if g i = a then (sgn i : ℤ) else 0) = f a :=
+begin
+  induction s using finset.cons_induction with a s ha ih generalizing n,
+  { exact ⟨0, classical.arbitrary _, λ _ _, rfl, λ _, false.elim⟩ },
+  rw sum_cons at hn,
+  obtain ⟨sgn, g, hg, hf⟩ := ih _ (le_tsub_of_add_le_left hn),
+  refine ⟨(range $ n - (f a).nat_abs).piecewise sgn (λ _, sign (f a)),
+    (range $ n - (f a).nat_abs).piecewise g (λ _, a), λ i hi, _, λ b hb, _⟩,
+  { by_cases i ∈ range (n - (f a).nat_abs),
+    { rw piecewise_eq_of_mem _ _ _ h at ⊢ hi,
+      exact hg _ (λ h, hi $ subset_cons _ h) },
+    { rw piecewise_eq_of_not_mem _ _ _ h at hi,
+      exact (hi $ mem_cons_self _ _).elim } },
+  transitivity ∑ i in range n, (range $ n - (f a).nat_abs).piecewise
+    (λ j, ite (g j = b) (sgn j : ℤ) 0) (λ j, ite (a = b) (sign $ f a) 0) i,
+  { exact sum_congr rfl (λ i _, exists_signed_sum_aux _ _ _ _) },
+  rw [sum_piecewise, (inter_eq_right_iff_subset _ _).2 (range_mono tsub_le_self)],
+  rw mem_cons at hb,
+  obtain rfl | hb := hb,
+  { rw [sum_eq_zero, zero_add, sum_const, if_pos rfl, card_sdiff (range_mono tsub_le_self),
+      card_range, card_range, tsub_tsub_cancel_of_le (le_of_add_le_left hn), nsmul_eq_mul, mul_comm,
+      ←int.sign_eq_sign, int.nat_cast_eq_coe_nat, (f b).sign_mul_nat_abs],
+    refine λ i hi, ite_eq_right_iff.2 _,
+    rintro rfl,
+    rw [hg _ ha, sign_type.coe_zero] },
+  { simp_rw [if_neg (ne_of_mem_of_not_mem hb ha).symm, hf _ hb, sum_const_zero, add_zero] }
+end

src/logic/nonempty.lean

@@ -112,6 +112,9 @@ h.elim $ f ∘ inhabited.mk
 instance {α β} [h : nonempty α] [h2 : nonempty β] : nonempty (α × β) :=
 h.elim $ λ g, h2.elim $ λ g2, ⟨⟨g, g2⟩⟩
 
+instance {α : Type*} {β : α → Type*} [h : Π a, nonempty (β a)] : nonempty (Π a, β a) :=
+⟨λ _, classical.arbitrary _⟩
+
 lemma subsingleton_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : subsingleton α :=
 ⟨λ x, false.elim $ not_nonempty_iff_imp_false.mp h x⟩