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 #
LinearMap.polar
: The polar of a bilinear formB : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
.
Main statements #
LinearMap.polar_eq_iInter
: The polar as an intersection.LinearMap.subset_bipolar
: The polar is a subset of the bipolar.LinearMap.polar_weak_closed
: The polar is closed in the weak topology induced byB.flip
.
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
.
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)
:
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)
:
@[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_nonempty
{𝕜 : 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).Nonempty
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}
:
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}
:
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 →ₗ[𝕜] 𝕜)
:
@[simp]
theorem
LinearMap.polar_singleton
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedCommRing 𝕜]
[AddCommMonoid E]
[AddCommMonoid F]
[Module 𝕜 E]
[Module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
{a : E}
:
theorem
LinearMap.mem_polar_singleton
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedCommRing 𝕜]
[AddCommMonoid E]
[AddCommMonoid F]
[Module 𝕜 E]
[Module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
{x : E}
(y : F)
:
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)
:
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 = (⨅ x ∈ m, LinearMap.ker (B x)).copy (B.polar ↑m) ⋯