Documentation

Mathlib.Analysis.LocallyConvex.Polar

Polar set #

In this file we define the polar set. There are different notions of the polar, we will define the absolute polar. The advantage over the real polar is that we can define the absolute polar for any bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, where 𝕜 is a normed commutative ring and E and F are modules over 𝕜.

Main definitions #

Main statements #

References #

Tags #

polar

def LinearMap.polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) :
Set F

The (absolute) polar of s : Set E is given by the set of all y : F such that ‖B x y‖ ≤ 1 for all x ∈ s.

Equations
  • B.polar s = {y : F | xs, (B x) y 1}
Instances For
    theorem LinearMap.polar_mem_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) (y : F) :
    y B.polar s xs, (B x) y 1
    theorem LinearMap.polar_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) (y : F) (hy : y B.polar s) (x : E) :
    x s(B x) y 1
    @[simp]
    theorem LinearMap.zero_mem_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) :
    0 B.polar s
    theorem LinearMap.polar_eq_iInter {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s : Set E} :
    B.polar s = xs, {y : F | (B x) y 1}
    theorem LinearMap.polar_gc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    GaloisConnection (OrderDual.toDual B.polar) (B.flip.polar OrderDual.ofDual)

    The map B.polar : Set E → Set F forms an order-reversing Galois connection with B.flip.polar : Set F → Set E. We use OrderDual.toDual and OrderDual.ofDual to express that polar is order-reversing.

    @[simp]
    theorem LinearMap.polar_iUnion {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {ι : Sort u_4} {s : ιSet E} :
    B.polar (⋃ (i : ι), s i) = ⋂ (i : ι), B.polar (s i)
    @[simp]
    theorem LinearMap.polar_union {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s : Set E} {t : Set E} :
    B.polar (s t) = B.polar s B.polar t
    theorem LinearMap.polar_antitone {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Antitone B.polar
    @[simp]
    theorem LinearMap.polar_empty {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    B.polar = Set.univ
    @[simp]
    theorem LinearMap.polar_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    B.polar {0} = Set.univ
    theorem LinearMap.subset_bipolar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) :
    s B.flip.polar (B.polar s)
    @[simp]
    theorem LinearMap.tripolar_eq_polar {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) :
    B.polar (B.flip.polar (B.polar s)) = B.polar s
    theorem LinearMap.polar_weak_closed {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedCommRing 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E) :
    IsClosed (B.polar s)

    The polar set is closed in the weak topology induced by B.flip.

    theorem LinearMap.polar_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (h : B.SeparatingRight) :
    B.polar Set.univ = {0}
    theorem LinearMap.polar_subMulAction {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {S : Type u_4} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
    B.polar m = {y : F | xm, (B x) y = 0}
    def LinearMap.polarSubmodule {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {S : Type u_4} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
    Submodule 𝕜 F

    The polar of a set closed under scalar multiplication as a submodule

    Equations
    • B.polarSubmodule m = (xm, LinearMap.ker (B x)).copy (B.polar m)
    Instances For