Pointwise operations on filters #
This file defines pointwise operations on filters. This is useful because usual algebraic operations distribute over pointwise operations. For example,
(f₁ * f₂).map m = f₁.map m * f₂.map m
𝓝 (x * y) = 𝓝 x * 𝓝 y
Main declarations #
0
(Filter.instZero
): Pure filter at0 : α
, or alternatively principal filter at0 : set α
.1
(Filter.instOne
): Pure filter at1 : α
, or alternatively principal filter at1 : set α
.f + g
(Filter.instAdd
): Addition, filter generated by alls + t
wheres ∈ f∈ f
andt ∈ g∈ g
.f * g
(Filter.instMul
): Multiplication, filter generated by alls * t
wheres ∈ f∈ f
andt ∈ g∈ g
.-f
(Filter.instNeg
): Negation, filter of all-s
wheres ∈ f∈ f
.f⁻¹⁻¹
(Filter.instInv
): Inversion, filter of alls⁻¹⁻¹
wheres ∈ f∈ f
.f - g
(Filter.instSub
): Subtraction, filter generated by alls - t
wheres ∈ f∈ f
andt ∈ g∈ g
.f / g
(Filter.instDiv
): Division, filter generated by alls / t
wheres ∈ f∈ f
andt ∈ g∈ g
.f +ᵥ g
(Filter.instVAdd
): Scalar addition, filter generated by alls +ᵥ t
wheres ∈ f∈ f
andt ∈ g∈ g
.f -ᵥ g
(Filter.instVSub
): Scalar subtraction, filter generated by alls -ᵥ t
wheres ∈ f∈ f
andt ∈ g∈ g
.f • g
(Filter.instSMul
): Scalar multiplication, filter generated by alls • t
wheres ∈ f∈ f
andt ∈ g∈ g
.a +ᵥ f
(Filter.instVAddFilter
): Translation, filter of alla +ᵥ s
wheres ∈ f∈ f
.a • f
(Filter.instSMulFilter
): Scaling, filter of alla • s
wheres ∈ f∈ f
.
For α
a semigroup/monoid, Filter α
is a semigroup/monoid.
As an unfortunate side effect, this means that n • f
, where n : ℕ
, is ambiguous between
pointwise scaling and repeated pointwise addition. See note [pointwise nat action].
Implementation notes #
We put all instances in the locale Pointwise
, so that these instances are not available by
default. Note that we do not mark them as reducible (as argued by note [reducible non-instances])
since we expect the locale to be open whenever the instances are actually used (and making the
instances reducible changes the behavior of simp
).
Tags #
filter multiplication, filter addition, pointwise addition, pointwise multiplication,
0
/1
as filters #
Filter negation/inversion #
The negation of a filter is the pointwise preimage under -
of its sets.
Equations
- Filter.instNeg = { neg := Filter.map Neg.neg }
The inverse of a filter is the pointwise preimage under ⁻¹⁻¹
of its sets.
Equations
- Filter.instInv = { inv := Filter.map Inv.inv }
Equations
- (_ : Filter.map Neg.neg (Filter.map Neg.neg f) = f) = (_ : Filter.map Neg.neg (Filter.map Neg.neg f) = f)
Negation is involutive on Filter α
if it is on α
.
Equations
- Filter.instInvolutiveNeg = let src := Filter.instNeg; InvolutiveNeg.mk (_ : ∀ (f : Filter α), Filter.map Neg.neg (Filter.map Neg.neg f) = f)
Inversion is involutive on Filter α
if it is on α
.
Equations
- Filter.instInvolutiveInv = let src := Filter.instInv; InvolutiveInv.mk (_ : ∀ (f : Filter α), Filter.map Inv.inv (Filter.map Inv.inv f) = f)
Filter addition/multiplication #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Filter subtraction/division #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a Filter
. See Note [pointwise nat action].
Filter α
is an AddSemigroup
under pointwise operations if α
is.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Filter.map₂ (fun x x_1 => x + x_1) x x = Filter.map₂ (fun x x_1 => x + x_1) x x) = (_ : Filter.map₂ (fun x x_1 => x + x_1) x x = Filter.map₂ (fun x x_1 => x + x_1) x x)
Filter α
is an AddCommSemigroup
under pointwise operations if α
is.
Equations
- One or more equations did not get rendered due to their size.
Filter α
is a CommSemigroup
under pointwise operations if α
is.
Equations
- Filter.commSemigroup = let src := Filter.semigroup; CommSemigroup.mk (_ : ∀ (x x_1 : Filter α), Filter.map₂ (fun x x_2 => x * x_2) x x_1 = Filter.map₂ (fun x x_2 => x * x_2) x_1 x)
Filter α
is an AddZeroClass
under pointwise operations if α
is.
Equations
- Filter.addZeroClass = AddZeroClass.mk (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x + x_1) (pure 0) l = l) (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x + x_1) l (pure 0) = l)
Filter α
is a MulOneClass
under pointwise operations if α
is.
Equations
- Filter.mulOneClass = MulOneClass.mk (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x * x_1) (pure 1) l = l) (_ : ∀ (l : Filter α), Filter.map₂ (fun x x_1 => x * x_1) l (pure 1) = l)
Equations
- (_ : Filter.map (↑φ) (x + x) = Filter.map (↑φ) x + Filter.map (↑φ) x) = (_ : Filter.map (↑φ) (x + x) = Filter.map (↑φ) x + Filter.map (↑φ) x)
Equations
- (_ : Filter.map (↑φ) 0 = 0) = (_ : Filter.map (↑φ) 0 = 0)
If φ : α →+ β→+ β
then mapAddMonoidHom φ
is the monoid homomorphism
Filter α →+ Filter β→+ Filter β
induced by map φ
.
Equations
- One or more equations did not get rendered due to their size.
If φ : α →* β→* β
then mapMonoidHom φ
is the monoid homomorphism
Filter α →* Filter β→* Filter β
induced by map φ
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
pure
as an AddMonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ZeroHom.toFun Filter.pureZeroHom 0 = 0) = (_ : ZeroHom.toFun Filter.pureZeroHom 0 = 0)
pure
as a MonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Filter.nsmul_mem_nsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n
Filter α
is an AddCommMonoid
under pointwise operations if α
is.
Filter α
is a CommMonoid
under pointwise operations if α
is.
Equations
- (_ : ∀ (x : Filter α), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : Filter α), AddMonoid.nsmul 0 x = 0)
Filter α
is a subtraction monoid under pointwise operations if
α
is.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a) = (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (n : ℕ) (x : Filter α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : Filter α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)
Equations
- One or more equations did not get rendered due to their size.
Filter α
is a division monoid under pointwise operations if α
is.
Equations
- One or more equations did not get rendered due to their size.
Filter α
is a commutative subtraction monoid under pointwise operations if α
is.
Filter α
is a commutative division monoid under pointwise operations if α
is.
Filter α
has distributive negation if α
has.
Equations
- One or more equations did not get rendered due to their size.
Note that Filter α
is not a Distrib
because f * g + f * h
has cross terms that f * (g + h)
lacks.
Note that Filter
is not a MulZeroClass
because 0 * ⊥ ≠ 0⊥ ≠ 0≠ 0
.
Note that Filter α
is not a group because f / f ≠ 1≠ 1
in general
Scalar addition/multiplication of filters #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Scalar subtraction of filters #
Translation/scaling of filters #
Equations
- (_ : CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass α (Filter β) (fun x x_1 => x +ᵥ x_1) fun x x_1 => x ≤ x_1)
Equations
- (_ : VAddCommClass α β (Filter γ)) = (_ : VAddCommClass α β (Filter γ))
Equations
- (_ : VAddCommClass α (Filter β) (Filter γ)) = (_ : VAddCommClass α (Filter β) (Filter γ))
Equations
- (_ : VAddCommClass (Filter α) β (Filter γ)) = (_ : VAddCommClass (Filter α) β (Filter γ))
Equations
- (_ : VAddCommClass (Filter α) (Filter β) (Filter γ)) = (_ : VAddCommClass (Filter α) (Filter β) (Filter γ))
Equations
- (_ : VAddAssocClass α β (Filter γ)) = (_ : VAddAssocClass α β (Filter γ))
Equations
- (_ : VAddAssocClass α (Filter β) (Filter γ)) = (_ : VAddAssocClass α (Filter β) (Filter γ))
Equations
- (_ : VAddAssocClass (Filter α) (Filter β) (Filter γ)) = (_ : VAddAssocClass (Filter α) (Filter β) (Filter γ))
Equations
- (_ : IsCentralVAdd α (Filter β)) = (_ : IsCentralVAdd α (Filter β))
Equations
- (_ : Filter.map₂ (fun x x_1 => x +ᵥ x_1) (pure 0) f = f) = (_ : Filter.map₂ (fun x x_1 => x +ᵥ x_1) (pure 0) f = f)
Equations
- One or more equations did not get rendered due to their size.
An additive action of an additive monoid α
on a type β
gives an additive action
of Filter α
on Filter β
Equations
- One or more equations did not get rendered due to their size.
A multiplicative action of a monoid α
on a type β
gives a multiplicative action of
Filter α
on Filter β
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Filter.map (fun x => 0 +ᵥ x) f = f) = (_ : Filter.map (fun x => 0 +ᵥ x) f = f)
A distributive multiplicative action of a monoid on an additive monoid β
gives a distributive
multiplicative action on Filter β
.
Equations
- One or more equations did not get rendered due to their size.
A multiplicative action of a monoid on a monoid β
gives a multiplicative action on set β
.
Equations
- One or more equations did not get rendered due to their size.
Note that we have neither SMulWithZero α (Filter β)
nor SMulWithZero (Filter α) (Filter β)
because 0 * ⊥ ≠ 0⊥ ≠ 0≠ 0
.