Flips of continuous pairings #
This file defines the continuous pairing obtained by exchanging the arguments of a jointly continuous continuous linear pairing, together with its evaluation and joint-continuity lemmas. Scalar multiplication is only assumed continuous for each fixed scalar.
noncomputable def
ContinuousLinearMap.pairingFlip
{G₁ : Type u_1}
{G₂ : Type u_2}
{G₃ : Type u_3}
[AddCommGroup G₁]
[Module ℝ G₁]
[TopologicalSpace G₁]
[AddCommGroup G₂]
[Module ℝ G₂]
[TopologicalSpace G₂]
[IsTopologicalAddGroup G₂]
[ContinuousConstSMul ℝ G₂]
[AddCommGroup G₃]
[Module ℝ G₃]
[TopologicalSpace G₃]
[IsTopologicalAddGroup G₃]
[ContinuousConstSMul ℝ G₃]
(μ : G₁ →L[ℝ] G₂ →L[ℝ] G₃)
(hμ : Continuous (Function.uncurry fun (x : G₁) (y : G₂) => (μ x) y))
:
The flipped continuous pairing obtained from a jointly continuous pairing.
The continuity hypothesis is needed because, outside the normed setting, joint continuity gives the required continuity of the curried map through the topology of bounded convergence.
Instances For
@[simp]
theorem
ContinuousLinearMap.pairingFlip_apply
{G₁ : Type u_1}
{G₂ : Type u_2}
{G₃ : Type u_3}
[AddCommGroup G₁]
[Module ℝ G₁]
[TopologicalSpace G₁]
[AddCommGroup G₂]
[Module ℝ G₂]
[TopologicalSpace G₂]
[IsTopologicalAddGroup G₂]
[ContinuousConstSMul ℝ G₂]
[AddCommGroup G₃]
[Module ℝ G₃]
[TopologicalSpace G₃]
[IsTopologicalAddGroup G₃]
[ContinuousConstSMul ℝ G₃]
(μ : G₁ →L[ℝ] G₂ →L[ℝ] G₃)
(hμ : Continuous (Function.uncurry fun (x : G₁) (y : G₂) => (μ x) y))
(x : G₂)
(y : G₁)
:
theorem
ContinuousLinearMap.pairingFlip_continuous
{G₁ : Type u_1}
{G₂ : Type u_2}
{G₃ : Type u_3}
[AddCommGroup G₁]
[Module ℝ G₁]
[TopologicalSpace G₁]
[AddCommGroup G₂]
[Module ℝ G₂]
[TopologicalSpace G₂]
[IsTopologicalAddGroup G₂]
[ContinuousConstSMul ℝ G₂]
[AddCommGroup G₃]
[Module ℝ G₃]
[TopologicalSpace G₃]
[IsTopologicalAddGroup G₃]
[ContinuousConstSMul ℝ G₃]
(μ : G₁ →L[ℝ] G₂ →L[ℝ] G₃)
(hμ : Continuous (Function.uncurry fun (x : G₁) (y : G₂) => (μ x) y))
:
Continuous (Function.uncurry fun (x : G₂) (y : G₁) => ((μ.pairingFlip hμ) x) y)
The flipped pairing is jointly continuous after exchanging the two arguments.