Documentation

Mathlib.Topology.Bornology.Absorbs

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:

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 MulDistribMulActions. They can be added later when someone needs them.

Keywords #

absorbs, absorbent

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

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
Instances For
    def Absorbent (M : Type u_1) {α : Type u_2} [Bornology M] [SMul M α] (s : Set α) :

    A set is absorbent if it absorbs every singleton.

    Equations
    Instances For
      theorem Absorbs.empty {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} :
      @[deprecated Absorbs.empty]
      theorem absorbs_empty {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} :

      Alias of Absorbs.empty.

      theorem Absorbs.eventually {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (h : Absorbs M s t) :
      ∀ᶠ (a : M) in Bornology.cobounded M, t a s
      @[simp]
      theorem Absorbs.of_boundedSpace {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} [BoundedSpace M] :
      Absorbs M s t
      theorem Absorbs.mono_left {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s₁ : Set α} {s₂ : Set α} {t : Set α} (h : Absorbs M s₁ t) (hs : s₁ s₂) :
      Absorbs M s₂ t
      theorem Absorbs.mono_right {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} (h : Absorbs M s t₁) (ht : t₂ t₁) :
      Absorbs M s t₂
      theorem Absorbs.mono {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (h : Absorbs M s₁ t₁) (hs : s₁ s₂) (ht : t₂ t₁) :
      Absorbs M s₂ t₂
      @[simp]
      theorem absorbs_union {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
      Absorbs M s (t₁ t₂) Absorbs M s t₁ Absorbs M s t₂
      theorem Absorbs.union {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} (h₁ : Absorbs M s t₁) (h₂ : Absorbs M s t₂) :
      Absorbs M s (t₁ t₂)
      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) tT, Absorbs M s t
      theorem Absorbs.sUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {T : Set (Set α)} (hT : T.Finite) (hs : tT, Absorbs M s t) :
      Absorbs M s (⋃₀ T)
      @[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)
      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.

      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 (⋃ iI, t i) iI, Absorbs M s (t i)
      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) :
      (∀ iI, Absorbs M s (t i))Absorbs M s (⋃ iI, t i)

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

      @[deprecated Set.Finite.absorbs_biUnion]
      theorem Set.Finite.absorbs_iUnion {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 (⋃ iI, t i) iI, Absorbs M s (t i)

      Alias of Set.Finite.absorbs_biUnion.

      @[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 (⋃ iI, t i) iI, Absorbs M s (t i)
      theorem Absorbs.biUnion_finset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : Finset ι} :
      (∀ iI, Absorbs M s (t i))Absorbs M s (⋃ iI, t i)

      Alias of the reverse direction of absorbs_biUnion_finset.

      @[deprecated absorbs_biUnion_finset]
      theorem absorbs_iUnion_finset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ιSet α} {I : Finset ι} :
      Absorbs M s (⋃ iI, t i) iI, Absorbs M s (t i)

      Alias of absorbs_biUnion_finset.

      theorem Absorbs.add {M : Type u_1} {E : Type u_2} [Bornology M] {s₁ : Set E} {s₂ : Set E} {t₁ : Set E} {t₂ : Set E} [AddZeroClass E] [DistribSMul M E] (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
      Absorbs M (s₁ + s₂) (t₁ + t₂)
      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
      @[simp]
      theorem Absorbs.univ {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} :
      Absorbs G₀ Set.univ s
      theorem absorbs_iff_eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} {t : Set α} :
      Absorbs G₀ s t ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun (x : α) => c⁻¹ x) t s
      theorem eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} {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.

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

      The filter of sets that absorb u.

      Equations
      Instances For
        @[simp]
        theorem Filter.mem_absorbing {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} {u : Set α} :
        s Filter.absorbing G₀ u Absorbs G₀ s u
        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 sS, Absorbs G₀ s t
        theorem Absorbs.sInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {S : Set (Set α)} (hS : S.Finite) :
        (∀ sS, Absorbs G₀ s t)Absorbs G₀ (⋂₀ S) t

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

        @[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
        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.

        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₀ (⋂ iI, s i) t iI, Absorbs G₀ (s i) t
        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 α} :
        (∀ iI, Absorbs G₀ (s i) t)Absorbs G₀ (⋂ iI, s i) t

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

        @[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
        @[simp]
        theorem absorbs_neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s : Set E} {t : Set E} :
        Absorbs M (-s) (-t) Absorbs M s t
        theorem Absorbs.of_neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s : Set E} {t : Set E} :
        Absorbs M (-s) (-t)Absorbs M s t

        Alias of the forward direction of absorbs_neg_neg.

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

        Alias of the reverse direction of absorbs_neg_neg.

        theorem Absorbs.sub {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s₁ : Set E} {s₂ : Set E} {t₁ : Set E} {t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
        Absorbs M (s₁ - s₂) (t₁ - t₂)
        theorem Absorbent.mono {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (ht : Absorbent M s) (hsub : s t) :
        @[deprecated Absorbent.mono]
        theorem Absorbent.subset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (ht : Absorbent M s) (hsub : s t) :

        Alias of Absorbent.mono.

        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}
        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}
        theorem Absorbent.absorbs_finite {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (hs : Absorbent M s) (ht : t.Finite) :
        Absorbs M s t
        theorem Absorbent.vadd_absorbs {M : Type u_1} {E : Type u_2} [Bornology M] [AddZeroClass E] [DistribSMul M E] {s₁ : Set E} {s₂ : Set E} {t : Set E} {x : E} (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) :
        Absorbs M (s₁ + s₂) (x +ᵥ t)
        theorem absorbent_univ {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] :
        Absorbent G₀ Set.univ
        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
        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
        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 : Set α} {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