Reorganising norms

Stream: general

[Yaël Dillies]

I have been doing background work to tidy up the material on norms and seminorms for a few weeks now, and I feel like I didn't expose my project enough.

So currently we have normed groups, rings, fields, modules on one hand and group, module seminorms on the other. The former are morally typeclass versions of the latter, so it would make sense for the classes to depend on the homs, but currently it's the other way around.

Hence I am trying to reduce imports for seminorms.

[Yaël Dillies]

There's also the fact that currently we have both the folders analysis.normed and analysis.normed_space. It makes sense to have groups, rings/fields, and modules/spaces separated because every time you add an operation: groups are + or *, rings/fields are + and *, modules/spaces are +, * and •.

Thus I am proposing the following folder organisation:

• analysis.normed
  • group
    • seminorm: Group norms and seminorms as homomorphisms (as is being moved in #16152, but the norms are missing).
    • basic: Group norms and seminorms as classes (as it is today).
  • ring or field
    • seminorm: Ring norms and seminorms as homomorphisms (as is being added in #14115).
    • basic: Ring norms and seminorms as classes (as it is today.
  • module or space
    • seminorm: Module norms and seminorms as homomorphisms (as it is in analysis.seminorm today, but the norms are missing).
    • basic: Ring norms and seminorms as classes (as it is in analysis.normed_space.basic today).

Every time, the .basic file would import the .seminorm file, rather than the other way around.

[Yaël Dillies]

Finally, we will be able to get rid of docs#seminormed_add_comm_group.core, which is just docs#add_group_seminorm again.

[Yaël Dillies]

cc @María Inés de Frutos Fernández, @Moritz Doll, @Eric Wieser

[Yaël Dillies]

My current plan of attack is

• reduce imports for add_group_seminorm/group_seminorm, move them to the correct place: #16152
• move other seminorms to the correct place
• remove seminormed_add_comm_group.core
• define ring (semi)norms: #14115
• define the missing norms
• remove normed_add_comm_group.core
• define noncommutative and multiplicative normed groups: #15705

[María Inés de Frutos Fernández]

This refactor sounds good. I am planning to add algebra_norm at some point (hopefully early September); normed_algebra could also be refactored in terms of it.

[Yaël Dillies]

Does that mean we should split the proposed analysis.normed.module folder into analysis.normed.module and analysis.normed.algebra?

[Yaël Dillies]

Also I just noticed that your add_group_seminorm has a redundant field :smile:

[María Inés de Frutos Fernández]

Yaël Dillies said:

Does that mean we should split the proposed analysis.normed.module folder into analysis.normed.module and analysis.normed.algebra?

Yes, I think that would be good. Also, the existing normed_algebra assumes an algebra over a normed_field, but I'd like the algebra_norm to allow algebras over normed_ring (these are used in nonarchimedean analysis).

[Kalle Kytölä]

If there will be a bigger refactor, then let me bring up an issue that I don't know how to solve elegantly in mathlib, and that has to do with (semi)norms (tangentially, at least).

The issue is that the type X →ᵇ ℝ≥0 of bounded continuous nnreal-valued functions currently doesn't have a multiplication. In current mathlib, has_mul (X →ᵇ R) is defined only under the assumption non_unital_semi_normed_ring R. Introducing something like non_unital_semi_normed_semiring might let us do a general enough case to include nonnegative functions, but this is not a very standard notion in real math, so I hesitate... Currently when I want to multiply bounded continuous nonnegative functions, I just do something like the code below, but this is ad hoc and too specific. Does someone see what is the correct mathlib way, and does it have any implications to the planned refactor of norms and seminorms?

import topology.continuous_function.bounded

noncomputable theory

open_locale bounded_continuous_function nnreal ennreal

variables {X : Type*} [topological_space X]

section quick_fixes_to_API_about_nnreal_valued_bounded_continuous_functions

-- Unrelated to the main issue, is this missing or did I just miss the relevant API?
lemma bounded_iff_dist_pt_bounded {α β : Type*} [metric_space β] (f : α → β) (z : β) :
  (∃ (C : ℝ), ∀ (x y : α), dist (f x) (f y) ≤ C) ↔ (∃ (B : ℝ), ∀ (x : α), dist (f x) z ≤ B) :=
begin
  split,
  { rintros ⟨C, hC⟩,
    by_cases is_empty α,
    { use C, exact h.elim, },
    simp only [not_is_empty_iff] at h,
    cases h with y,
    use C + (dist (f y) z),
    intros x,
    apply (dist_triangle (f x) (f y) z).trans,
    simpa only [add_le_add_iff_right] using hC x y, },
  { rintros ⟨B, hB⟩,
    use 2*B,
    intros x y,
    apply (dist_triangle (f x) z (f y)).trans,
    rw dist_comm z _,
    apply (add_le_add (hB x) (hB y)).trans (le_of_eq _),
    ring, },
end

/- This is an ad hoc fix. There should be a `has_mul (X →ᵇ R)` with general enough
typeclasses to apply to the case `R = ℝ≥0`. Mathlib's current typeclasses for this are not
general enough: `bounded_continuous_function.has_mul` assumes `non_unital_semi_normed_ring R`. -/
def bounded_continuous_function.nnreal_mul {α : Type*} [topological_space α] (f g : α →ᵇ ℝ≥0) :
  α →ᵇ ℝ≥0 :=
{ to_fun := λ x, f x * g x,
  continuous_to_fun := f.continuous.mul g.continuous,
  map_bounded' := begin
    apply (bounded_iff_dist_pt_bounded (λ x, f x * g x) 0).mpr,
    rcases (bounded_iff_dist_pt_bounded f 0).mp f.bounded with ⟨A, hf⟩,
    rcases (bounded_iff_dist_pt_bounded g 0).mp g.bounded with ⟨B, hg⟩,
    use A*B,
    intros x,
    simp_rw [dist_nndist, nnreal.nndist_zero_eq_val', nnreal.coe_mul] at *,
    exact mul_le_mul (hf x) (hg x) (g x).coe_nonneg ((f x).coe_nonneg.trans (hf x)),
  end }

end quick_fixes_to_API_about_nnreal_valued_bounded_continuous_functions --section

[Kalle Kytölä]

There is also a similar issue with subtraction in X →ᵇ ℝ≥0. The current assumption of has_sub (X →ᵇ R) is seminormed_add_comm_group R; we don't have seminormed_add_comm_semigroup to define has_tsub (X →ᵇ R) :stuck_out_tongue_wink:. More seriously --- does someone see the good long term solution? (Ad hoc fixes like the above are obviously again possible.)

[Yaël Dillies]

I think non_unital_seminormed_semiring is the way. After all, real maths doesn't really care about ℝ≥0 in the first place!

[Yaël Dillies]

This is somewhat orthogonal to the current discussion, however.

[Kalle Kytölä]

Yaël Dillies said:

I think non_unital_seminormed_semiring is the way.

... and seminormed_add_comm_semigroup for the truncated subtraction of nonnegative bounded continuous functions?

[Yaël Dillies]

Maybe! But please wait for #15705 or I will go insane :rofl:
(I have been working on making branch#normed_group compile for the past month)

[Kalle Kytölä]

Sure! I am certainly not rushing to define non_unital_seminormed_semirings or seminormed_add_comm_semigroups :grinning_face_with_smiling_eyes:. My main point now was to mention these issues we have noticed, in case they have any implications for the ongoing refactor.

[Jireh Loreaux]

Just FYI, I think you will have problems here. First of all, notice that you actually want the comm versions. And note that #13719 is stuck (partly because I'm dreading how many timeouts I'm going to have to fix in order to get it to build)

[Jireh Loreaux]

(I mean technical problems, not mathematical or design problems.)

[Yaël Dillies]

The current state of affairs:

• #16152: Move group seminorms
• #16227: Switch seminorms to the new homs design
• #16228: positivity extension for seminorms
• #16237: Group norms
• #16238: Get rid of docs#seminormed_add_comm_group.core and docs#normed_add_comm_group.core
• #15705: Multiplicative, noncommutative normed groups

Each one depends on the previous (except #16228 that's a spinoff).

[Yaël Dillies]

The first two at least are uncontroversial, so would be good to get them in soon.

[Yaël Dillies]

#16227 is easy and ready. It adds hom classes for seminorms.

[Filippo A. E. Nuccio]

And is there any room for introducing quasinorms in this refactor? This has already been discussed sometimes and @Heather Macbeth and myself might need them (although for the time being we follow a different path).

[Yaël Dillies]

Yes absolutely! Do you care about quasinorms (aka bundled homs mike docs#seminorm), or quasinormed spaces (aka typeclasses, like docs#seminormed_add_comm_group), or both?

[Filippo A. E. Nuccio]

Well, the long-term goal is to prove the Aoki--Rolewicz theorem saying that quasi-Banach and $p$-Banach are equivalent categories, see here, page 1. I would say that having the definitions of quasinorms would already be great, quasi-Banach can come later.

[Yaël Dillies]

I feel like this can be done with either quasinorms or quasinormed spaces.

[Yury G. Kudryashov]

Historical note: a while ago, we had analysis.normed_space. Then I started moving stuff to newly created normed.* but got distracted and didn't finish the refactoring.

[Filippo A. E. Nuccio]

At any rate, I am trying to develop something about quasi-normed space on a personal branch (which is still a complete mess). As soon as I get something that will look reasonable, I will discuss it here.

[Anatole Dedecker]

@Yaël Dillies I would like to get a docs#seminormed_add_comm_group instance form a docs#add_group_seminorm (I think we don't have this yet, did I miss it?). How would that fit in your plan? Will I get that from free from your refactor, or is this orthogonal, and in that case how should I define it to fit your changes?

[Yaël Dillies]

It's #16238, which is ready for review!

[Anatole Dedecker]

Nice, thanks!

[Anatole Dedecker]

There are conflicts in this PR btw, in case you didn’t notice

[Yaël Dillies]

Oh thanks! I was pretty sure I had checked.