-
Notifications
You must be signed in to change notification settings - Fork 251
/
NeLocus.lean
180 lines (136 loc) · 6.78 KB
/
NeLocus.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
/-
Copyright (c) 2022 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import Mathlib.Data.Finsupp.Defs
#align_import data.finsupp.ne_locus from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"
/-!
# Locus of unequal values of finitely supported functions
Let `α N` be two Types, assume that `N` has a `0` and let `f g : α →₀ N` be finitely supported
functions.
## Main definition
* `Finsupp.neLocus f g : Finset α`, the finite subset of `α` where `f` and `g` differ.
In the case in which `N` is an additive group, `Finsupp.neLocus f g` coincides with
`Finsupp.support (f - g)`.
-/
variable {α M N P : Type*}
namespace Finsupp
variable [DecidableEq α]
section NHasZero
variable [DecidableEq N] [Zero N] (f g : α →₀ N)
/-- Given two finitely supported functions `f g : α →₀ N`, `Finsupp.neLocus f g` is the `Finset`
where `f` and `g` differ. This generalizes `(f - g).support` to situations without subtraction. -/
def neLocus (f g : α →₀ N) : Finset α :=
(f.support ∪ g.support).filter fun x => f x ≠ g x
#align finsupp.ne_locus Finsupp.neLocus
@[simp]
theorem mem_neLocus {f g : α →₀ N} {a : α} : a ∈ f.neLocus g ↔ f a ≠ g a := by
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
and_iff_right_iff_imp] using Ne.ne_or_ne _
#align finsupp.mem_ne_locus Finsupp.mem_neLocus
theorem not_mem_neLocus {f g : α →₀ N} {a : α} : a ∉ f.neLocus g ↔ f a = g a :=
mem_neLocus.not.trans not_ne_iff
#align finsupp.not_mem_ne_locus Finsupp.not_mem_neLocus
@[simp]
theorem coe_neLocus : ↑(f.neLocus g) = { x | f x ≠ g x } := by
ext
exact mem_neLocus
#align finsupp.coe_ne_locus Finsupp.coe_neLocus
@[simp]
theorem neLocus_eq_empty {f g : α →₀ N} : f.neLocus g = ∅ ↔ f = g :=
⟨fun h =>
ext fun a => not_not.mp (mem_neLocus.not.mp (Finset.eq_empty_iff_forall_not_mem.mp h a)),
fun h => h ▸ by simp only [neLocus, Ne, eq_self_iff_true, not_true, Finset.filter_False]⟩
#align finsupp.ne_locus_eq_empty Finsupp.neLocus_eq_empty
@[simp]
theorem nonempty_neLocus_iff {f g : α →₀ N} : (f.neLocus g).Nonempty ↔ f ≠ g :=
Finset.nonempty_iff_ne_empty.trans neLocus_eq_empty.not
#align finsupp.nonempty_ne_locus_iff Finsupp.nonempty_neLocus_iff
theorem neLocus_comm : f.neLocus g = g.neLocus f := by
simp_rw [neLocus, Finset.union_comm, ne_comm]
#align finsupp.ne_locus_comm Finsupp.neLocus_comm
@[simp]
theorem neLocus_zero_right : f.neLocus 0 = f.support := by
ext
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
#align finsupp.ne_locus_zero_right Finsupp.neLocus_zero_right
@[simp]
theorem neLocus_zero_left : (0 : α →₀ N).neLocus f = f.support :=
(neLocus_comm _ _).trans (neLocus_zero_right _)
#align finsupp.ne_locus_zero_left Finsupp.neLocus_zero_left
end NHasZero
section NeLocusAndMaps
theorem subset_mapRange_neLocus [DecidableEq N] [Zero N] [DecidableEq M] [Zero M] (f g : α →₀ N)
{F : N → M} (F0 : F 0 = 0) : (f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g :=
fun x => by simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F
#align finsupp.subset_map_range_ne_locus Finsupp.subset_mapRange_neLocus
theorem zipWith_neLocus_eq_left [DecidableEq N] [Zero M] [DecidableEq P] [Zero P] [Zero N]
{F : M → N → P} (F0 : F 0 0 = 0) (f : α →₀ M) (g₁ g₂ : α →₀ N)
(hF : ∀ f, Function.Injective fun g => F f g) :
(zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂ := by
ext
simpa only [mem_neLocus] using (hF _).ne_iff
#align finsupp.zip_with_ne_locus_eq_left Finsupp.zipWith_neLocus_eq_left
theorem zipWith_neLocus_eq_right [DecidableEq M] [Zero M] [DecidableEq P] [Zero P] [Zero N]
{F : M → N → P} (F0 : F 0 0 = 0) (f₁ f₂ : α →₀ M) (g : α →₀ N)
(hF : ∀ g, Function.Injective fun f => F f g) :
(zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂ := by
ext
simpa only [mem_neLocus] using (hF _).ne_iff
#align finsupp.zip_with_ne_locus_eq_right Finsupp.zipWith_neLocus_eq_right
theorem mapRange_neLocus_eq [DecidableEq N] [DecidableEq M] [Zero M] [Zero N] (f g : α →₀ N)
{F : N → M} (F0 : F 0 = 0) (hF : Function.Injective F) :
(f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g := by
ext
simpa only [mem_neLocus] using hF.ne_iff
#align finsupp.map_range_ne_locus_eq Finsupp.mapRange_neLocus_eq
end NeLocusAndMaps
variable [DecidableEq N]
@[simp]
theorem neLocus_add_left [AddLeftCancelMonoid N] (f g h : α →₀ N) :
(f + g).neLocus (f + h) = g.neLocus h :=
zipWith_neLocus_eq_left _ _ _ _ add_right_injective
#align finsupp.ne_locus_add_left Finsupp.neLocus_add_left
@[simp]
theorem neLocus_add_right [AddRightCancelMonoid N] (f g h : α →₀ N) :
(f + h).neLocus (g + h) = f.neLocus g :=
zipWith_neLocus_eq_right _ _ _ _ add_left_injective
#align finsupp.ne_locus_add_right Finsupp.neLocus_add_right
section AddGroup
variable [AddGroup N] (f f₁ f₂ g g₁ g₂ : α →₀ N)
@[simp]
theorem neLocus_neg_neg : neLocus (-f) (-g) = f.neLocus g :=
mapRange_neLocus_eq _ _ neg_zero neg_injective
#align finsupp.ne_locus_neg_neg Finsupp.neLocus_neg_neg
theorem neLocus_neg : neLocus (-f) g = f.neLocus (-g) := by rw [← neLocus_neg_neg, neg_neg]
#align finsupp.ne_locus_neg Finsupp.neLocus_neg
theorem neLocus_eq_support_sub : f.neLocus g = (f - g).support := by
rw [← neLocus_add_right _ _ (-g), add_right_neg, neLocus_zero_right, sub_eq_add_neg]
#align finsupp.ne_locus_eq_support_sub Finsupp.neLocus_eq_support_sub
@[simp]
theorem neLocus_sub_left : neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂ := by
simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]
#align finsupp.ne_locus_sub_left Finsupp.neLocus_sub_left
@[simp]
theorem neLocus_sub_right : neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂ := by
simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _
#align finsupp.ne_locus_sub_right Finsupp.neLocus_sub_right
@[simp]
theorem neLocus_self_add_right : neLocus f (f + g) = g.support := by
rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]
#align finsupp.ne_locus_self_add_right Finsupp.neLocus_self_add_right
@[simp]
theorem neLocus_self_add_left : neLocus (f + g) f = g.support := by
rw [neLocus_comm, neLocus_self_add_right]
#align finsupp.ne_locus_self_add_left Finsupp.neLocus_self_add_left
@[simp]
theorem neLocus_self_sub_right : neLocus f (f - g) = g.support := by
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
#align finsupp.ne_locus_self_sub_right Finsupp.neLocus_self_sub_right
@[simp]
theorem neLocus_self_sub_left : neLocus (f - g) f = g.support := by
rw [neLocus_comm, neLocus_self_sub_right]
#align finsupp.ne_locus_self_sub_left Finsupp.neLocus_self_sub_left
end AddGroup
end Finsupp