Compatible additive group norms

Two additive group norms bounded by constant multiples of one another induce the same uniformity. AddGroupNorm.toNormedAddCommGroupOfUniformity installs a new norm while retaining the original uniformity and topology definitionally. In particular, existing completeness and continuity proofs remain usable. This construction is shared by adapted and rounded norms.

theorem AddGroupNorm.uniformity_eq_of_le {M : Type u_1} [NormedAddCommGroup M] (N : AddGroupNorm M) {C D : NNReal} (h₁ : ∀ (x : M), N x ≤ ↑C * ‖x‖) (h₂ : ∀ (x : M), ‖x‖ ≤ ↑D * N x) : uniformity M = uniformity M

An additive group norm bounded-equivalent to the original norm induces its uniformity.

@[reducible, inline]

noncomputable abbrev AddGroupNorm.toNormedAddCommGroupOfUniformity {M : Type u_1} [NormedAddCommGroup M] (N : AddGroupNorm M) (h : uniformity M = uniformity M) : NormedAddCommGroup M

Install an additive group norm with the original uniformity and topology retained definitionally. Thus completeness and continuity are unchanged.

theorem AddGroupNorm.norm_toNormedAddCommGroupOfUniformity {M : Type u_1} [NormedAddCommGroup M] (N : AddGroupNorm M) (h : uniformity M = uniformity M) (x : M) : ‖x‖ = N x

The compatible structure has the specified additive group norm.