Basic lemmas on normed scalar actions and modules

This file collects elementary facts about scalar actions on seminormed additive groups and real normed spaces:

• RingHomIsometric.intCastRingHom: in a seminormed ring in which ℤ acts isometrically and ‖1‖ = 1, such as ℝ or ℂ, Int.castRingHom R preserves norms, making lemmas stated for a RingHomIsometric ring homomorphism (such as Polynomial.supNorm_map) apply to integer polynomials.
• TauCeti.norm_sum_smul_le_sum_div_mul: when scalar coefficients satisfy ‖a i‖ * r i ≤ b against positive weights r i, the combination ∑ i ∈ s, a i • u i has norm at most (∑ i ∈ s, ‖u i‖ / r i) * b; in particular, strict-generator representations yield uniformly norm-bounded preimages along linear maps.
• TauCeti.norm_smul_sq_div_add_norm_smul_sq: the ratio ‖u‖² / (‖u‖² + ‖v‖²) is unchanged when u and v are scaled by the same nonzero scalar.
• TauCeti.mul_norm_le_two_mul_norm_of_norm_sub_smul_le: a vector within K * a ^ 2 of the real multiple a • v, with |a| * (2 * K) ≤ ‖v‖, still has norm at least half of |a| * ‖v‖.
• IsOpen.diam_pos: a nonempty bounded open set in a nontrivial real normed space has positive diameter.

instance RingHomIsometric.intCastRingHom {R : Type u_1} [SeminormedRing R] [NormSMulClass ℤ R] [NormOneClass R] : RingHomIsometric (Int.castRingHom R)

The cast from ℤ is norm-preserving in a normed ring in which ℤ acts isometrically and ‖1‖ = 1, such as ℝ or ℂ.

theorem TauCeti.norm_sum_smul_le_sum_div_mul {ι : Type u_1} {A : Type u_2} {E : Type u_3} [SeminormedAddGroup A] [SeminormedAddCommGroup E] [SMulZeroClass A E] [IsBoundedSMul A E] {s : Finset ι} {r : ι → ℝ} (hr : ∀ i ∈ s, 0 < r i) {u : ι → E} {a : ι → A} {b : ℝ} (ha : ∀ i ∈ s, ‖a i‖ * r i ≤ b) : ‖∑ i ∈ s, a i • u i‖ ≤ (∑ i ∈ s, ‖u i‖ / r i) * b

If scalar coefficients a i satisfy ‖a i‖ * r i ≤ b against positive weights r i, then ‖∑ i ∈ s, a i • u i‖ ≤ (∑ i ∈ s, ‖u i‖ / r i) * b.

theorem TauCeti.norm_smul_sq_div_add_norm_smul_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SeminormedAddCommGroup F] [Module 𝕜 F] [NormSMulClass 𝕜 F] (u : E) (v : F) {t : 𝕜} (ht : t ≠ 0) : ‖t • u‖ ^ 2 / (‖t • u‖ ^ 2 + ‖t • v‖ ^ 2) = ‖u‖ ^ 2 / (‖u‖ ^ 2 + ‖v‖ ^ 2)

The ratio ‖u‖² / (‖u‖² + ‖v‖²) is unchanged when u and v are scaled by the same nonzero scalar.

theorem TauCeti.mul_norm_le_two_mul_norm_of_norm_sub_smul_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {z v : E} {a K : ℝ} (hR : ‖z - a • v‖ ≤ K * a ^ 2) (ha : |a| * (2 * K) ≤ ‖v‖) : |a| * ‖v‖ ≤ 2 * ‖z‖

A quadratic error cannot swallow the linear term. If z lies within K * a ^ 2 of the real multiple a • v, and a is small enough that |a| * (2 * K) ≤ ‖v‖, then z still inherits half of the length |a| * ‖v‖ of that multiple.

theorem IsOpen.diam_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {s : Set E} (hs : IsOpen s) (hb : Bornology.IsBounded s) {x : E} (hx : x ∈ s) : 0 < Metric.diam s

A nonempty bounded open set in a nontrivial real normed space has positive diameter.