refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Remove injectiveSeminorm

[goliath-klein]

Currently, injectiveSeminorm is extensionally equal to projectiveSeminorm. Both implement what is commonly called the "projective tensor norm".

Background

(C.f. [Diestel et al.]). On the algebraic tensor product of two Banach spaces X, Y, there are two distinguished norms. First the projective norm, or "largest reasonable crossnorm". Two equivalent expressions for it are:

(L1) ‖u‖_∧ = sup { sum_i ‖x_i‖ ‖y_i‖ | sum_i x_i ⊗ y_i = u },
(L2) ‖u‖_∧ = norm of the linear map that sends b : B(X,Y; 𝕂) to (lift b) u,

where B(X,Y; Z) is the set of bounded bilinear maps into a normed space Z.

Second, there is the injective norm, or "smallest reasonable crossnorm":

(S) ‖u‖_∨ = norm of the bilinear map that sends f : X', g : Y' to (f⊗g) u.

Mathlib

The formalization treats tensor products of seminormed spaces over normed fields. In this context, projectiveSeminorm implements (L1). But injectiveSeminorm u doesn't implement (S), but the following variant of (L2):

(L2') sup_Z { norm of map sending b : B(X,Y; Z) to (lift b) u }.

In fact, injectiveSeminorm = projectiveSeminorm . The upper bound is proven in Mathlib. Equality is attained (somewhat tautologically) by choosing Z to be X ⊗ Y endowed with the projective seminorm.

projectiveSeminorm is defined first; injectiveSeminorm builds on it. Then the theory of an isometric version of PiTensorProduct.lift is based on injectiveSeminorm.

Proposed change

This PR deprecates injectiveSeminorm and ports all applications to (L1). This doesn't actually require too much work, leads to the same mathematical theory, and significantly reduces complexity (and potential for confusion!).

There is a companion PR which formalizes the equality of the current definitions and has a WIP / RFC implementation of the injective seminorm as commonly understood.

Deprecations:

• injectiveSeminorm
• injectiveSeminorm_apply
• norm_eval_le_injectiveSeminorm
• injectiveSeminorm_le_projectiveSeminorm
• injectiveSeminorm_tprod_le
• Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

---

Co-authored-by: Davood H. H. Tehrani

[github-actions]

PR summary d3153cf426

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ injectiveSeminorm_eq_projectiveSeminorm
+ instance (x : ⨂[R] i, s i) : Nonempty ↑x.lifts := nonempty_subtype.mpr (nonempty_lifts x)
+ instance : Norm (⨂[𝕜] i, E i)
+ instance : NormedSpace 𝕜 (⨂[𝕜] i, E i) := ⟨projectiveSeminorm_smul_le⟩
+ norm_def
+ projectiveSeminorm_add_le
+ projectiveSeminorm_smul_le
+ projectiveSeminorm_zero
+ projectiveSeminorn_mem_dualSeminorms
- instance : NormedSpace 𝕜 (⨂[𝕜] i, E i)
- projectiveSeminorm_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (3.00, 0.15)

Current number	Change	Type
20	3	disabled deprecation lints

Current commit c2f8d1af25
Reference commit d3153cf426

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Ruben-VandeVelde]

Please keep the file (with deprecated_module) and mark all declarations as deprecated rather than removing them outright. We can decide what to do with the deprecations once the other PR is ready.

awaiting-author

[goliath-klein]

Please keep the file (with deprecated_module) and mark all declarations as deprecated rather than removing them outright. We can decide what to do with the deprecations once the other PR is ready.

Thanks for the comment! Done.

Notes:

• The old proof of norm_eval_le_injectiveSeminorm fails after the refactor due to type class problems. Presumably that's because the norm instance for PiTensorProduct is now registered earlier (in ProjectiveSeminorm.lean), while previously it was registered after the theorem. Rather than debugging a soon-to-be-deprecated proof, I copied over injectiveSeminorm_eq_projectiveSeminorm from the other PR and based the proof on that stronger result. (It's still shorter than before).
• The deprecation attributes carry comments rather than alternative definitions, even in cases like injectiveSeminorm where deprecated projectiveSeminorm would have made sense. That's because I've also slightly weakened assumptions, which led to warnings because the types of the definitions don't strictly match.
• I've also moved some definitions temporarily back to InjectiveSeminorm.lean for review, so that git diff can pick up the changes more cleanly. All non-deprecated definitions should be moved to ProjectiveSeminorm.lean before merge.

-awaiting-author

[dupuisf]

Wouldn't it be useful to keep the former definition of injectiveSeminorm around as an alternative characterization of the projective seminorm?

[dupuisf]

Is this really useless now?

[goliath-klein]

You're right, that was premature.

Some version of the construction will definitely be needed. There's a much shorter definition at the WIP PR, which directly gives a continuous linear map. But it isn't yet clear whether this will make the linear version redundant. I have therefore removed to deprecation note for now.

[goliath-klein]

Thanks! To better address the comments, let me add some material over at the WIP PR.

awaiting-author

[goliath-klein]

Wouldn't it be useful to keep the former definition of injectiveSeminorm around as an alternative characterization of the projective seminorm?

One could do that. In this case, one should prove the equivalence of the characterization directly rather than rely on the old code. Over at the WIP PR, I've included a concise proof as projectiveSeminorm_dual_characterization.

Arguments in favor:

• It's now short and it exists already, so why not.

Arguments against (in the language of the PR description at the top):

• The interesting direction is (L2') ≤ (L1), which would be included anyway (and doesn't have the unnatural universe constraints which are required for the converse). And the converse is somewhat tautological: It arises by choosing the normed space Z equal to the PiTensorProduct already endowed with the projective seminorm.
• Under weak additional assumptions (such as [RCLike 𝕜]), the optimization over normed spaces Z is not even necessary. I've now included projectiveSeminorm_of_bidual_iso which shows that the supremum is attained for Z = 𝕜 if the PiTensorProduct embeds isometrically into the bidual.

Either way is fine by me. What do you think?

In any case, I think it makes sense to proceed step by step. This PR removes the duplicate definition and ports the existing results to projectiveSeminorm. Both projectiveSeminorm_of_bidual_iso and projectiveSeminorm_dual_characterization (if wanted) are new material. We'll submit those later, as significant work remains to be done.

-awaiting-author

[tb65536]

I don't think this is the correct thing to do here? There's a lot of this file that isn't being deprecated.

[tb65536]

Later if you want to deprecate this file, you should move things out first, I think.

[tb65536]

(This could be a TODO)

[robin-carlier]

It seems this PR is doing two things at the same time: modifying things in projective seminorms, and then deprecating all the stuff about injective seminorms.

To make this easier to review, can you please separate the part that refactors the projective seminorm, and then make a second PR doing the deprecations, linking to the first one and the zulip discussion? This way, the second PR would be an easy merge. Or was the point that the changes in the projective seminorms are breaking proofs in the injective ones?

[goliath-klein]

Thanks, Robin, Thomas for your comments.

Let me try to disentangle things.

Current status:

• The actual injective seminorm does not exist in Mathlib.
• The projective seminorm is formalized twice, once under the name projectiveSeminorm and once (confusingly) under the name injectiveSeminorm. The definitions are propositionally, but not definitionally equal.
• Some properties of the projective seminorm are proven for the projectiveSeminorm definition, some for the injectiveSeminorm definition.

Short-term goal (this PR):

• Deprecate the injectiveSeminorm definition, which is both redundant and non-standard.
• Reprove all properties in terms of projectiveSeminorm, which is the standard definition.

Mid-term goal (WIP):

• Formalize the actual injective seminorm.

With this in mind, the following considerations went into this PR:

• I've ported around 170 lines of code in InjectiveSeminorm.lean (between liftEquiv and mapLMultilinear_opNorm) from injectiveSeminorm to projectiveSeminorm. These new versions eventually belong into ProjectiveSeminorm.lean. But for the purpose of the review I've left them in their old place. That's because the changes are comparatively minor, so that reviewing them should be much easier if one can see the diff. (I've mentioned this in a comment, but probably not prominently enough. Sorry).
• I don't think one can separate this PR into one "modify ProjectiveSeminorm.lean" and one "deprecate InjectiveSeminorm.lean" step. The latter file imports the former, so all the definitions that I've ported from injective to projective would cause conflicts, as would the Norm instance that's now registered already in ProjectiveSeminorm.lean. (So, yes, there would be breakage, as Robin suspected).

Options for proceeding:

• I leave things as they are, having finally explained the strategy sufficiently clearly. (Sorry for earlier confusion).
• I move all definitions that are meant to stay over to their final destination in ProjectiveSeminorm.lean, leaving only deprecated stuff in InjectiveSeminorm.lean. Pro: Easier structure. Con: diff doesn't pick up on the many lines that didn't change.
• Other ideas?

[goliath-klein]

-awaiting-author

[goliath-klein]

Also, maybe I should say more clearly that injectiveSeminorm is arguably a "misformalization" in the sense that it does not implement the concept it is named after.

It is thus very unlikely that any downstream project builds on it: Anyone who wanted to use it would have realized that it doesn't do what it says on the tin (as happened to us). This also means that the details of the deprecation strategy might not be as relevant in this case as they would generally be.

[tb65536]

But presumably you could do the deprecation in one PR, and then make the changes to ProjectiveSeminorm in a subsequent PR?

[goliath-klein]

@tb65536: One issue would be that there are plenty of definitions that are currently stated in terms of injectiveSeminorm that I'm porting over to projectiveSeminorm. What should happen to those if injectiveSeminorm is deprecated before the port is complete?

Zooming out, do I understand everyone's comments correctly as saying that it would be helpful if the PR got split into smaller and less noisy pieces?

If so, I could split it up like this:

1. The minor golfs I've applied throughout.
2. Mark results about injectiveSeminorm as deprecated if nothing builds on them.
3. Main step: Change the Norm instance to projectiveSeminorm and port all definitions to projectiveSeminorm.
4. Move ported definitions to ProjectiveSeminorm.lean; mark injectiveSeminorm and the module as deprecated.

Would that be helpful?

[tb65536]

Yes, that sort of splitting up would be helpful if possible.