Weak dual topology #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the weak topology given two vector spaces E and F over a commutative semiring
𝕜 and a bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜. The weak topology on E is the coarsest topology
such that for all y : F every map λ x, B x y is continuous.
In the case that F = E →L[𝕜] 𝕜 and B being the canonical pairing, we obtain the weak-* topology,
weak_dual 𝕜 E := (E →L[𝕜] 𝕜). Interchanging the arguments in the bilinear form yields the
weak topology weak_space 𝕜 E := E.
Main definitions #
The main definitions are the types weak_bilin B for the general case and the two special cases
weak_dual 𝕜 E and weak_space 𝕜 E with the respective topology instances on it.
- Given
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, the typeweak_bilin Bis a type synonym forE. - The instance
weak_bilin.topological_spaceis the weak topology induced by the bilinear formB. weak_dual 𝕜 Eis a type synonym fordual 𝕜 E(when the latter is defined): both are equal to the typeE →L[𝕜] 𝕜of continuous linear maps from a moduleEover𝕜to the ring𝕜.- The instance
weak_dual.topological_spaceis the weak-* topology onweak_dual 𝕜 E, i.e., the coarsest topology making the evaluation maps at allz : Econtinuous. weak_space 𝕜 Eis a type synonym forE(when the latter is defined).- The instance
weak_dual.topological_spaceis the weak topology onE, i.e., the coarsest topology such that allv : dual 𝕜 Eremain continuous.
Main results #
We establish that weak_bilin B has the following structure:
weak_bilin.has_continuous_add: The addition inweak_bilin Bis continuous.weak_bilin.has_continuous_smul: The scalar multiplication inweak_bilin Bis continuous.
We prove the following results characterizing the weak topology:
eval_continuous: For anyy : F, the evaluation mappingλ x, B x yis continuous.continuous_of_continuous_eval: For a mapping toweak_bilin Bto be continuous, it suffices that its compositions with pairing withBat all pointsy : Fis continuous.tendsto_iff_forall_eval_tendsto: Convergence inweak_bilin Bcan be characterized in terms of convergence of the evaluations at all pointsy : F.
Notations #
No new notation is introduced.
References #
Tags #
weak-star, weak dual, duality
@[protected, instance]
def
weak_bilin.add_comm_monoid
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
@[protected, instance]
def
weak_bilin.module
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
module 𝕜 (weak_bilin B)
@[nolint]
def
weak_bilin
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
Type u_5
The space E equipped with the weak topology induced by the bilinear form B.
Equations
- weak_bilin B = E
@[protected, instance]
def
weak_bilin.add_comm_group
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[a : add_comm_group E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
Equations
@[protected, instance]
def
weak_bilin.module'
{𝕜 : Type u_2}
{𝕝 : Type u_3}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[comm_semiring 𝕝]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
[m : module 𝕝 E]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
module 𝕝 (weak_bilin B)
Equations
- weak_bilin.module' B = m
@[protected, instance]
def
weak_bilin.is_scalar_tower
{𝕜 : Type u_2}
{𝕝 : Type u_3}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[comm_semiring 𝕝]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
[has_smul 𝕝 𝕜]
[module 𝕝 E]
[s : is_scalar_tower 𝕝 𝕜 E]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
is_scalar_tower 𝕝 𝕜 (weak_bilin B)
@[protected, instance]
def
weak_bilin.topological_space
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
Equations
- weak_bilin.topological_space B = topological_space.induced (λ (x : weak_bilin B) (y : F), ⇑(⇑B x) y) Pi.topological_space
theorem
weak_bilin.coe_fn_continuous
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
continuous (λ (x : weak_bilin B) (y : F), ⇑(⇑B x) y)
The coercion (λ x y, B x y) : E → (F → 𝕜) is continuous.
theorem
weak_bilin.eval_continuous
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
(y : F) :
continuous (λ (x : weak_bilin B), ⇑(⇑B x) y)
theorem
weak_bilin.continuous_of_continuous_eval
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
[topological_space α]
{g : α → weak_bilin B}
(h : ∀ (y : F), continuous (λ (a : α), ⇑(⇑B (g a)) y)) :
theorem
weak_bilin.embedding
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
{B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜}
(hB : function.injective ⇑B) :
embedding (λ (x : weak_bilin B) (y : F), ⇑(⇑B x) y)
The coercion (λ x y, B x y) : E → (F → 𝕜) is an embedding.
theorem
weak_bilin.tendsto_iff_forall_eval_tendsto
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
{l : filter α}
{f : α → weak_bilin B}
{x : weak_bilin B}
(hB : function.injective ⇑B) :
filter.tendsto f l (nhds x) ↔ ∀ (y : F), filter.tendsto (λ (i : α), ⇑(⇑B (f i)) y) l (nhds (⇑(⇑B x) y))
@[protected, instance]
def
weak_bilin.has_continuous_add
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
[has_continuous_add 𝕜] :
Addition in weak_space B is continuous.
@[protected, instance]
def
weak_bilin.has_continuous_smul
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[add_comm_monoid F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
[has_continuous_smul 𝕜 𝕜] :
Scalar multiplication by 𝕜 on weak_bilin B is continuous.
@[protected, instance]
def
weak_bilin.topological_add_group
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[topological_space 𝕜]
[comm_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
(B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
[has_continuous_add 𝕜] :
weak_space B is a topological_add_group, meaning that addition and negation are
continuous.
def
top_dual_pairing
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
[has_continuous_const_smul 𝕜 𝕜] :
The canonical pairing of a vector space and its topological dual.
Equations
theorem
dual_pairing_apply
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
(v : E →L[𝕜] 𝕜)
(x : E) :
⇑(⇑(top_dual_pairing 𝕜 E) v) x = ⇑v x
@[protected, instance]
def
weak_dual.add_comm_monoid
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
add_comm_monoid (weak_dual 𝕜 E)
@[protected, instance]
def
weak_dual.module
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
def
weak_dual
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
Type (max u_2 u_1)
The weak star topology is the topology coarsest topology on E →L[𝕜] 𝕜 such that all
functionals λ v, top_dual_pairing 𝕜 E v x are continuous.
Equations
- weak_dual 𝕜 E = weak_bilin (top_dual_pairing 𝕜 E)
Instances for weak_dual
- weak_dual.add_comm_monoid
- weak_dual.module
- weak_dual.topological_space
- weak_dual.has_continuous_add
- weak_dual.inhabited
- weak_dual.weak_dual.continuous_linear_map_class
- weak_dual.has_coe_to_fun
- weak_dual.mul_action
- weak_dual.distrib_mul_action
- weak_dual.module'
- weak_dual.has_continuous_const_smul
- weak_dual.has_continuous_smul
- weak_dual.t2_space
@[protected, instance]
def
weak_dual.has_continuous_add
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
has_continuous_add (weak_dual 𝕜 E)
@[protected, instance]
def
weak_dual.topological_space
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
topological_space (weak_dual 𝕜 E)
@[protected, instance]
def
weak_dual.inhabited
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
@[protected, instance]
def
weak_dual.weak_dual.continuous_linear_map_class
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
continuous_linear_map_class (weak_dual 𝕜 E) 𝕜 E 𝕜
@[protected, instance]
def
weak_dual.has_coe_to_fun
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
has_coe_to_fun (weak_dual 𝕜 E) (λ (_x : weak_dual 𝕜 E), E → 𝕜)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
@[protected, instance]
def
weak_dual.mul_action
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
(M : Type u_1)
[monoid M]
[distrib_mul_action M 𝕜]
[smul_comm_class 𝕜 M 𝕜]
[has_continuous_const_smul M 𝕜] :
mul_action M (weak_dual 𝕜 E)
If a monoid M distributively continuously acts on 𝕜 and this action commutes with
multiplication on 𝕜, then it acts on weak_dual 𝕜 E.
Equations
@[protected, instance]
def
weak_dual.distrib_mul_action
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
(M : Type u_1)
[monoid M]
[distrib_mul_action M 𝕜]
[smul_comm_class 𝕜 M 𝕜]
[has_continuous_const_smul M 𝕜] :
distrib_mul_action M (weak_dual 𝕜 E)
If a monoid M distributively continuously acts on 𝕜 and this action commutes with
multiplication on 𝕜, then it acts distributively on weak_dual 𝕜 E.
@[protected, instance]
def
weak_dual.module'
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
(R : Type u_1)
[semiring R]
[module R 𝕜]
[smul_comm_class 𝕜 R 𝕜]
[has_continuous_const_smul R 𝕜] :
If 𝕜 is a topological module over a semiring R and scalar multiplication commutes with the
multiplication on 𝕜, then weak_dual 𝕜 E is a module over R.
Equations
@[protected, instance]
def
weak_dual.has_continuous_const_smul
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
(M : Type u_1)
[monoid M]
[distrib_mul_action M 𝕜]
[smul_comm_class 𝕜 M 𝕜]
[has_continuous_const_smul M 𝕜] :
has_continuous_const_smul M (weak_dual 𝕜 E)
@[protected, instance]
def
weak_dual.has_continuous_smul
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
(M : Type u_1)
[monoid M]
[distrib_mul_action M 𝕜]
[smul_comm_class 𝕜 M 𝕜]
[topological_space M]
[has_continuous_smul M 𝕜] :
has_continuous_smul M (weak_dual 𝕜 E)
If a monoid M distributively continuously acts on 𝕜 and this action commutes with
multiplication on 𝕜, then it continuously acts on weak_dual 𝕜 E.
theorem
weak_dual.coe_fn_continuous
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
continuous (λ (x : weak_dual 𝕜 E) (y : E), ⇑x y)
theorem
weak_dual.eval_continuous
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
(y : E) :
continuous (λ (x : weak_dual 𝕜 E), ⇑x y)
theorem
weak_dual.continuous_of_continuous_eval
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
[topological_space α]
{g : α → weak_dual 𝕜 E}
(h : ∀ (y : E), continuous (λ (a : α), ⇑(g a) y)) :
@[protected, instance]
def
weak_dual.t2_space
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
[t2_space 𝕜] :
@[protected, instance]
def
weak_space.has_continuous_add
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
has_continuous_add (weak_space 𝕜 E)
@[protected, instance]
def
weak_space.module
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
module 𝕜 (weak_space 𝕜 E)
@[protected, instance]
def
weak_space.add_comm_monoid
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
add_comm_monoid (weak_space 𝕜 E)
@[protected, instance]
def
weak_space.topological_space
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
topological_space (weak_space 𝕜 E)
@[nolint]
def
weak_space
(𝕜 : Type u_1)
(E : Type u_2)
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
Type u_2
The weak topology is the topology coarsest topology on E such that all
functionals λ x, top_dual_pairing 𝕜 E v x are continuous.
Equations
- weak_space 𝕜 E = weak_bilin (top_dual_pairing 𝕜 E).flip
Instances for weak_space
def
weak_space.map
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
[add_comm_monoid F]
[module 𝕜 F]
[topological_space F]
(f : E →L[𝕜] F) :
weak_space 𝕜 E →L[𝕜] weak_space 𝕜 F
A continuous linear map from E to F is still continuous when E and F are equipped with
their weak topologies.
Equations
- weak_space.map f = {to_linear_map := f.to_linear_map, cont := _}
theorem
weak_space.map_apply
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
[add_comm_monoid F]
[module 𝕜 F]
[topological_space F]
(f : E →L[𝕜] F)
(x : E) :
⇑(weak_space.map f) x = ⇑f x
@[simp]
theorem
weak_space.coe_map
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
[add_comm_monoid F]
[module 𝕜 F]
[topological_space F]
(f : E →L[𝕜] F) :
⇑(weak_space.map f) = ⇑f
theorem
tendsto_iff_forall_eval_tendsto_top_dual_pairing
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_5}
[comm_semiring 𝕜]
[topological_space 𝕜]
[has_continuous_add 𝕜]
[has_continuous_const_smul 𝕜 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E]
{l : filter α}
{f : α → weak_dual 𝕜 E}
{x : weak_dual 𝕜 E} :
filter.tendsto f l (nhds x) ↔ ∀ (y : E), filter.tendsto (λ (i : α), ⇑(⇑(top_dual_pairing 𝕜 E) (f i)) y) l (nhds (⇑(⇑(top_dual_pairing 𝕜 E) x) y))