Documentation

Mathlib.Analysis.LocallyConvex.AbsConvex

Absolutely convex sets #

A set s in an commutative monoid E is called absolutely convex or disked if it is convex and balanced. The importance of absolutely convex sets comes from the fact that every locally convex topological vector space has a basis consisting of absolutely convex sets.

Main definitions #

Main statements #

Tags #

disks, convex, balanced

def AbsConvex (π•œ : Type u_1) {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] (s : Set E) :

A set is absolutely convex if it is balanced and convex.

Equations
Instances For
    theorem AbsConvex.empty {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] :
    AbsConvex π•œ βˆ…
    theorem AbsConvex.univ {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] :
    theorem AbsConvex.inter {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s t : Set E} (hs : AbsConvex π•œ s) (ht : AbsConvex π•œ t) :
    AbsConvex π•œ (s ∩ t)
    theorem AbsConvex.sInter {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {S : Set (Set E)} (h : βˆ€ s ∈ S, AbsConvex π•œ s) :
    AbsConvex π•œ (β‹‚β‚€ S)
    theorem AbsConvex.iInter {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {ΞΉ : Sort u_3} {s : ΞΉ β†’ Set E} (h : βˆ€ (i : ΞΉ), AbsConvex π•œ (s i)) :
    AbsConvex π•œ (β‹‚ (i : ΞΉ), s i)
    theorem AbsConvex.iInterβ‚‚ {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {ΞΉ : Sort u_3} {ΞΊ : ΞΉ β†’ Sort u_4} {f : (i : ΞΉ) β†’ ΞΊ i β†’ Set E} (h : βˆ€ (i : ΞΉ) (j : ΞΊ i), AbsConvex π•œ (f i j)) :
    AbsConvex π•œ (β‹‚ (i : ΞΉ), β‹‚ (j : ΞΊ i), f i j)
    def absConvexHull (π•œ : Type u_1) {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] :

    The absolute convex hull of a set s is the minimal absolute convex set that includes s.

    Equations
    Instances For
      @[simp]
      theorem absConvexHull_isClosed (π•œ : Type u_1) {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] (s : Set E) :
      (absConvexHull π•œ).IsClosed s = AbsConvex π•œ s
      theorem subset_absConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      s βŠ† (absConvexHull π•œ) s
      theorem absConvex_absConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      AbsConvex π•œ ((absConvexHull π•œ) s)
      theorem balanced_absConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      Balanced π•œ ((absConvexHull π•œ) s)
      theorem convex_absConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      Convex π•œ ((absConvexHull π•œ) s)
      theorem absConvexHull_eq_iInter (π•œ : Type u_1) {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] (s : Set E) :
      (absConvexHull π•œ) s = β‹‚ (t : Set E), β‹‚ (_ : s βŠ† t), β‹‚ (_ : AbsConvex π•œ t), t
      theorem mem_absConvexHull_iff {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} {x : E} :
      x ∈ (absConvexHull π•œ) s ↔ βˆ€ (t : Set E), s βŠ† t β†’ AbsConvex π•œ t β†’ x ∈ t
      theorem absConvexHull_min {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s t : Set E} :
      s βŠ† t β†’ AbsConvex π•œ t β†’ (absConvexHull π•œ) s βŠ† t
      theorem AbsConvex.absConvexHull_subset_iff {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s t : Set E} (ht : AbsConvex π•œ t) :
      (absConvexHull π•œ) s βŠ† t ↔ s βŠ† t
      theorem absConvexHull_mono {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s t : Set E} (hst : s βŠ† t) :
      (absConvexHull π•œ) s βŠ† (absConvexHull π•œ) t
      theorem absConvexHull_eq_self {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      (absConvexHull π•œ) s = s ↔ AbsConvex π•œ s
      theorem AbsConvex.absConvexHull_eq {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      AbsConvex π•œ s β†’ (absConvexHull π•œ) s = s

      Alias of the reverse direction of absConvexHull_eq_self.

      @[simp]
      theorem absConvexHull_univ {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] :
      @[simp]
      theorem absConvexHull_empty {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] :
      @[simp]
      theorem absConvexHull_eq_empty {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      @[simp]
      theorem absConvexHull_nonempty {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      theorem Set.Nonempty.absConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] {s : Set E} :
      s.Nonempty β†’ ((absConvexHull π•œ) s).Nonempty

      Alias of the reverse direction of absConvexHull_nonempty.

      theorem absConvex_closed_sInter {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {S : Set (Set E)} (h : βˆ€ s ∈ S, AbsConvex π•œ s ∧ IsClosed s) :
      def closedAbsConvexHull (π•œ : Type u_1) {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] :

      The absolutely convex closed hull of a set s is the minimal absolutely convex closed set that includes s.

      Equations
      Instances For
        @[simp]
        theorem closedAbsConvexHull_isClosed (π•œ : Type u_1) {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] (s : Set E) :
        theorem absConvex_convexClosedHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {s : Set E} :
        AbsConvex π•œ ((closedAbsConvexHull π•œ) s)
        theorem isClosed_closedAbsConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {s : Set E} :
        theorem subset_closedAbsConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {s : Set E} :
        theorem closure_subset_closedAbsConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {s : Set E} :
        theorem closedAbsConvexHull_min {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {s t : Set E} (hst : s βŠ† t) (h_conv : AbsConvex π•œ t) (h_closed : IsClosed t) :
        theorem absConvexHull_subset_closedAbsConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {s : Set E} :
        (absConvexHull π•œ) s βŠ† (closedAbsConvexHull π•œ) s
        @[simp]
        theorem closedAbsConvexHull_closure_eq_closedAbsConvexHull {π•œ : Type u_1} {E : Type u_2} [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ] [TopologicalSpace E] {s : Set E} :
        (closedAbsConvexHull π•œ) (closure s) = (closedAbsConvexHull π•œ) s
        theorem AbsConvex.closure {π•œ : Type u_1} {E : Type u_2} [NormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul π•œ E] {s : Set E} (hs : AbsConvex π•œ s) :
        theorem closedAbsConvexHull_eq_closure_absConvexHull {π•œ : Type u_1} {E : Type u_2} [NormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul π•œ E] {s : Set E} :
        (closedAbsConvexHull π•œ) s = closure ((absConvexHull π•œ) s)
        theorem nhds_hasBasis_absConvex (π•œ : Type u_1) (E : Type u_2) [NontriviallyNormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [LocallyConvexSpace π•œ E] [ContinuousSMul π•œ E] :
        (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ AbsConvex π•œ s) id
        theorem nhds_hasBasis_absConvex_open (π•œ : Type u_1) (E : Type u_2) [NontriviallyNormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [LocallyConvexSpace π•œ E] [ContinuousSMul π•œ E] [IsTopologicalAddGroup E] [ZeroLEOneClass π•œ] :
        (nhds 0).HasBasis (fun (s : Set E) => 0 ∈ s ∧ IsOpen s ∧ AbsConvex π•œ s) id
        theorem absConvexHull_add_subset (π•œ : Type u_1) {E : Type u_2} [NontriviallyNormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] {s t : Set E} :
        (absConvexHull π•œ) (s + t) βŠ† (absConvexHull π•œ) s + (absConvexHull π•œ) t
        theorem absConvexHull_eq_convexHull_balancedHull (π•œ : Type u_1) {E : Type u_2} [NontriviallyNormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} :
        (absConvexHull π•œ) s = (convexHull π•œ) (balancedHull π•œ s)
        theorem balancedHull_convexHull_subseteq_absConvexHull (π•œ : Type u_1) {E : Type u_2} [NontriviallyNormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} :
        balancedHull π•œ ((convexHull π•œ) s) βŠ† (absConvexHull π•œ) s

        In general, equality doesn't hold here - e.g. consider s := {(-1, 1), (1, 1)} in ℝ².

        theorem zero_mem_absConvexHull {π•œ : Type u_1} {E : Type u_2} {s : Set E} [SeminormedRing π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] [Nonempty ↑s] :
        0 ∈ (absConvexHull π•œ) s