# Absorption of sets #

Let `M` act on `α`, let `A` and `B` be sets in `α`. We say that `A` absorbs `B` if for sufficiently large `a : M`, we have `B ⊆ a • A`. Formally, "for sufficiently large `a : M`" means "for all but a bounded set of `a`".

Traditionally, this definition is formulated for the action of a (semi)normed ring on a module over that ring.

We formulate it in a more general settings for two reasons:

- this way we don't have to depend on metric spaces, normed rings etc;
- some proofs look nicer with this definition than with something like `∃ r : ℝ, ∀ a : R, r ≤ ‖a‖ → B ⊆ a • A`.

If `M` is a `GroupWithZero` (e.g., a division ring), the sets absorbing a given set form a filter, see `Filter.absorbing`.

## Implementation notes #

For now, all theorems assume that we deal with (a generalization of) a module over a division ring. Some lemmas have multiplicative versions for `MulDistribMulAction`s. They can be added later when someone needs them.

## Keywords #

absorbs, absorbent

source
def Absorbs (M : Type u_1) {α : Type u_2} [Bornology M] [SMul M α] (s t : Set α) :
Prop

A set `s` absorbs another set `t` if `t` is contained in all scalings of `s` by all but a bounded set of elements.

Equations

- Absorbs M s t = ∀ᶠ (a : M) in Bornology.cobounded M, t ⊆ a • s

Instances For

source
def Absorbent (M : Type u_1) {α : Type u_2} [Bornology M] [SMul M α] (s : Set α) :
Prop

A set is absorbent if it absorbs every singleton.

Equations

- Absorbent M s = ∀ (x : α), Absorbs M s {x}

Instances For

source
theorem Absorbs.empty {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} :
Absorbs M s ∅
source
theorem Absorbs.eventually {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s t : Set α} (h : Absorbs M s t) :
∀ᶠ (a : M) in Bornology.cobounded M, t ⊆ a • s
source
@[simp]
theorem Absorbs.of_boundedSpace {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s t : Set α} [BoundedSpace M] :
Absorbs M s t
source
theorem Absorbs.mono_left {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s₁ s₂ t : Set α} (h : Absorbs M s₁ t) (hs : s₁ ⊆ s₂) :
Absorbs M s₂ t
source
theorem Absorbs.mono_right {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s t₁ t₂ : Set α} (h : Absorbs M s t₁) (ht : t₂ ⊆ t₁) :
Absorbs M s t₂
source
theorem Absorbs.mono {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s₁ s₂ t₁ t₂ : Set α} (h : Absorbs M s₁ t₁) (hs : s₁ ⊆ s₂) (ht : t₂ ⊆ t₁) :
Absorbs M s₂ t₂
source
@[simp]
theorem absorbs_union {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s t₁ t₂ : Set α} :
Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂
source
theorem Absorbs.union {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s t₁ t₂ : Set α} (h₁ : Absorbs M s t₁) (h₂ : Absorbs M s t₂) :
Absorbs M s (t₁ ∪ t₂)
source
theorem Set.Finite.absorbs_sUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {T : Set (Set α)} (hT : T.Finite) :
Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t
source
theorem Absorbs.sUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {T : Set (Set α)} (hT : T.Finite) (hs : ∀ t ∈ T, Absorbs M s t) :
Absorbs M s (⋃₀ T)
source
@[simp]
theorem absorbs_iUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Sort u_3} [Finite ι] {t : ι → Set α} :
Absorbs M s (⋃ (i : ι), t i) ↔ ∀ (i : ι), Absorbs M s (t i)
source
theorem Absorbs.iUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Sort u_3} [Finite ι] {t : ι → Set α} :
(∀ (i : ι), Absorbs M s (t i)) → Absorbs M s (⋃ (i : ι), t i)

Alias of the reverse direction of `absorbs_iUnion`.

source
theorem Set.Finite.absorbs_biUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Set ι} (hI : I.Finite) :
Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)
source
theorem Absorbs.biUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Set ι} (hI : I.Finite) :
(∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)

Alias of the reverse direction of `Set.Finite.absorbs_biUnion`.

source
@[simp]
theorem absorbs_biUnion_finset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Finset ι} :
Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)
source
theorem Absorbs.biUnion_finset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Finset ι} :
(∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)

Alias of the reverse direction of `absorbs_biUnion_finset`.

source
theorem Absorbs.add {M : Type u_1} {E : Type u_2} [Bornology M] {s₁ s₂ t₁ t₂ : Set E} [AddZeroClass E] [DistribSMul M E] (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
Absorbs M (s₁ + s₂) (t₁ + t₂)
source
theorem Absorbs.zero {M : Type u_1} {E : Type u_2} [Bornology M] [Zero E] [SMulZeroClass M E] {s : Set E} (hs : 0 ∈ s) :
Absorbs M s 0
source
@[simp]
theorem Absorbs.univ {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} :
Absorbs G₀ Set.univ s
source
theorem absorbs_iff_eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s t : Set α} :
Absorbs G₀ s t ↔ ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun (x : α) => c⁻¹ • x) t s
source
theorem eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s t : Set α} :
Absorbs G₀ s t → ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun (x : α) => c⁻¹ • x) t s

Alias of the forward direction of `absorbs_iff_eventually_cobounded_mapsTo`.

source
@[simp]
theorem absorbs_inter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s t u : Set α} :
Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u
source
theorem Absorbs.inter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s t u : Set α} (hs : Absorbs G₀ s u) (ht : Absorbs G₀ t u) :
Absorbs G₀ (s ∩ t) u
source
def Filter.absorbing (G₀ : Type u_1) {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] (u : Set α) :
Filter α

The filter of sets that absorb `u`.

Equations

- Filter.absorbing G₀ u = { sets := {s : Set α | Absorbs G₀ s u}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Instances For

source
@[simp]
theorem Filter.mem_absorbing {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s u : Set α} :
s ∈ absorbing G₀ u ↔ Absorbs G₀ s u
source
theorem Set.Finite.absorbs_sInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {S : Set (Set α)} (hS : S.Finite) :
Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t
source
theorem Absorbs.sInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {S : Set (Set α)} (hS : S.Finite) :
(∀ s ∈ S, Absorbs G₀ s t) → Absorbs G₀ (⋂₀ S) t

Alias of the reverse direction of `Set.Finite.absorbs_sInter`.

source
@[simp]
theorem absorbs_iInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Sort u_3} [Finite ι] {s : ι → Set α} :
Absorbs G₀ (⋂ (i : ι), s i) t ↔ ∀ (i : ι), Absorbs G₀ (s i) t
source
theorem Absorbs.iInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Sort u_3} [Finite ι] {s : ι → Set α} :
(∀ (i : ι), Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ (i : ι), s i) t

Alias of the reverse direction of `absorbs_iInter`.

source
theorem Set.Finite.absorbs_biInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t
source
theorem Absorbs.biInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
(∀ i ∈ I, Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ i ∈ I, s i) t

Alias of the reverse direction of `Set.Finite.absorbs_biInter`.

source
@[simp]
theorem absorbs_zero_iff {G₀ : Type u_1} [GroupWithZero G₀] [Bornology G₀] [(Bornology.cobounded G₀).NeBot] {E : Type u_3} [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} :
Absorbs G₀ s 0 ↔ 0 ∈ s
source
@[simp]
theorem absorbs_neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s t : Set E} :
Absorbs M (-s) (-t) ↔ Absorbs M s t
source
theorem Absorbs.neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s t : Set E} :
Absorbs M s t → Absorbs M (-s) (-t)

Alias of the reverse direction of `absorbs_neg_neg`.

source
theorem Absorbs.of_neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s t : Set E} :
Absorbs M (-s) (-t) → Absorbs M s t

Alias of the forward direction of `absorbs_neg_neg`.

source
theorem Absorbs.sub {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s₁ s₂ t₁ t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
Absorbs M (s₁ - s₂) (t₁ - t₂)
source
theorem Absorbent.mono {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s t : Set α} (ht : Absorbent M s) (hsub : s ⊆ t) :
Absorbent M t
source
theorem absorbent_iff_forall_absorbs_singleton {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} :
Absorbent M s ↔ ∀ (x : α), Absorbs M s {x}
source
theorem Absorbent.absorbs {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} (hs : Absorbent M s) {x : α} :
Absorbs M s {x}
source
theorem Absorbent.absorbs_finite {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s t : Set α} (hs : Absorbent M s) (ht : t.Finite) :
Absorbs M s t
source
theorem Absorbent.vadd_absorbs {M : Type u_1} {E : Type u_2} [Bornology M] [AddZeroClass E] [DistribSMul M E] {s₁ s₂ t : Set E} {x : E} (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) :
Absorbs M (s₁ + s₂) (x +ᵥ t)
source
theorem absorbent_univ {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] :
Absorbent G₀ Set.univ
source
theorem absorbent_iff_inv_smul {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} :
Absorbent G₀ s ↔ ∀ (x : α), ∀ᶠ (c : G₀) in Bornology.cobounded G₀, c⁻¹ • x ∈ s
source
theorem Absorbent.zero_mem {G₀ : Type u_1} {E : Type u_3} [GroupWithZero G₀] [Bornology G₀] [(Bornology.cobounded G₀).NeBot] [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} (hs : Absorbent G₀ s) :
0 ∈ s
source
theorem Absorbs.restrict_scalars {M : Type u_1} {N : Type u_2} {α : Type u_3} [Monoid N] [SMul M N] [SMul M α] [MulAction N α] [IsScalarTower M N α] [Bornology M] [Bornology N] {s t : Set α} (h : Absorbs N s t) (hbdd : Filter.Tendsto (fun (x : M) => x • 1) (Bornology.cobounded M) (Bornology.cobounded N)) :
Absorbs M s t