feat: continuous linear equivalence between continuous ℝ- and 𝕜-linear functionals (in either the strong or weak-⋆ topologies)#34728
Conversation
…inear functionals, when equipped with the weak⋆-topology
PR summary 9d0ea7dd98
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.Normed.Module.RCLike.Extend | 1713 | 1718 | +5 (+0.29%) |
| Mathlib.Analysis.Normed.Module.WeakDual | 2159 | 2160 | +1 (+0.05%) |
Import changes for all files
| Files | Import difference |
|---|---|
4 filesMathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.HahnBanach Mathlib.Analysis.Normed.Module.WeakDual |
1 |
Mathlib.Analysis.Normed.Module.RCLike.Extend |
5 |
Declarations diff
+ _root_.StrongDual.toWeakDual_extendRCLikeₗ_apply
+ _root_.WeakBilin.continuous_of_continuous_eval_re
+ continuous_of_continuous_eval_re
+ extendRCLikeL_apply_apply
+ extendRCLikeL_symm_apply_apply
+ toContinuousLinearEquiv_extendRCLikeₗᵢ
+ toStrongDual_extendRCLikeL_apply
++ extendRCLikeL
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (1.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 10188 | 1 | backward.isDefEq |
Current commit d27852e8ac
Reference commit 9d0ea7dd98
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
j-loreaux
changed the title
ℝ and 𝕜-linear functionals, when equipped with the weak⋆-topology
j-loreaux
changed the title
ℝ and 𝕜-linear functionals, when equipped with the weak⋆-topologyℝ- and 𝕜-linear functionals, when equipped with the weak⋆-topology
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
mathlib-dependent-issues
bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
github-actions
bot
removed
the
merge-conflict
j-loreaux
changed the title
ℝ- and 𝕜-linear functionals, when equipped with the weak⋆-topologyℝ- and 𝕜-linear functionals (in either the strong or weak-⋆ topologies)
|
@urkud this is the follow up to the PR containing the |
|
Not strictly related, but do we agree that the sentence "It would be possible to use LinearMap.mkContinuous here, but we would need to know that the continuity of fr implies it has bounded norm and we want to avoid that dependency here." in the docstring of StrongDual.extendRCLike is misleading because there is no longer any norm around? |
|
@ADedecker Sure, I can delete it in this PR if you would like, or do it in a separate one. |
4 participants
This realizes the map
StrongDual.extendRCLikeₗ, after pre- and post-composing so that it is an equivalence between the weak duals, as a continuous linear equivalence.In addition, when the space is a topological vector space, we realize
StrongDual.extendRCLikeₗas a continuous linear equivalence between the strong duals.ℝ- and𝕜-linear functionals #34543The placement in
Analysis/Normed/Module/WeakDualseems suboptimal because this has nothing to do with the norm. This is becauseWeakDual.toStrongDualis already in this file, which should probably be moved toTopology/Algebra/Module/WeakDual. However, even if that moves, the declarations added in this PR cannot easily go with it because they involveRCLike. Potentially, they could move toAnalysis/RCLike/Extendif that file gained theTopology/Algebra/Module/WeakDualimport.