Normalizing continuous linear equivalences

The file also bounds the inverse of a continuous linear equivalence from a quadratic lower bound on the equivalence itself.

Rescaling a continuous linear equivalence T between normed spaces by a nonzero scalar does not change ‖T‖ * ‖T⁻¹‖. Using Mathlib's rescale_to_shell, every equivalence from a nonzero space can be rescaled to have norm at most 1, with its inverse then of norm at most ‖c‖ * ‖T‖ * ‖T⁻¹‖ for any scalar c with 1 < ‖c‖. This bounds both operators at once, as needed in compactness arguments over the set of equivalences.

For finite index types S and T, the splitting ContinuousLinearEquiv.sumPiEquivProdPi of a family indexed by S ⊕ T into its restrictions to S and to T preserves the sup norms (ContinuousLinearEquiv.norm_sumPiEquivProdPi_apply), so it and its inverse have operator norm at most 1.

theorem ContinuousLinearEquiv.exists_norm_le_one_and_norm_symm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Nontrivial E] {c : 𝕜} (hc : 1 < ‖c‖) (T : E ≃L[𝕜] F) : ∃ (U : E ≃L[𝕜] F), ‖↑U‖ ≤ 1 ∧ ‖↑U.symm‖ ≤ ‖c‖ * (‖↑T‖ * ‖↑T.symm‖) ∧ ‖↑U‖ * ‖↑U.symm‖ = ‖↑T‖ * ‖↑T.symm‖

Given a scalar with 1 < ‖c‖, every continuous linear equivalence T from a nonzero space can be rescaled, without changing ‖T‖ * ‖T⁻¹‖, to have norm at most 1 and inverse of norm at most ‖c‖ * ‖T‖ * ‖T⁻¹‖.

theorem ContinuousLinearEquiv.norm_sumPiEquivProdPi_apply {S : Type u_4} {T : Type u_5} [Fintype S] [Fintype T] {A : S ⊕ T → Type u_6} [(st : S ⊕ T) → SeminormedAddCommGroup (A st)] (R : Type u_7) [Semiring R] [(st : S ⊕ T) → Module R (A st)] (x : (st : S ⊕ T) → A st) : ‖(sumPiEquivProdPi R S T A) x‖ = ‖x‖

Splitting a family indexed by S ⊕ T into its restrictions to S and to T preserves the sup norm.

theorem ContinuousLinearEquiv.norm_sumPiEquivProdPi_symm_apply {S : Type u_4} {T : Type u_5} [Fintype S] [Fintype T] {A : S ⊕ T → Type u_6} [(st : S ⊕ T) → SeminormedAddCommGroup (A st)] (R : Type u_7) [Semiring R] [(st : S ⊕ T) → Module R (A st)] (p : ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))) : ‖(sumPiEquivProdPi R S T A).symm p‖ = ‖p‖

Gluing a family on S and a family on T into a family on S ⊕ T preserves the sup norm.

theorem ContinuousLinearEquiv.opNorm_sumPiEquivProdPi_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {S : Type u_4} {T : Type u_5} [Fintype S] [Fintype T] {A : S ⊕ T → Type u_6} [(st : S ⊕ T) → SeminormedAddCommGroup (A st)] [(st : S ⊕ T) → NormedSpace 𝕜 (A st)] : ‖↑(sumPiEquivProdPi 𝕜 S T A)‖ ≤ 1

The splitting sumPiEquivProdPi has operator norm at most 1.

theorem ContinuousLinearEquiv.opNorm_sumPiEquivProdPi_symm_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {S : Type u_4} {T : Type u_5} [Fintype S] [Fintype T] {A : S ⊕ T → Type u_6} [(st : S ⊕ T) → SeminormedAddCommGroup (A st)] [(st : S ⊕ T) → NormedSpace 𝕜 (A st)] : ‖↑(sumPiEquivProdPi 𝕜 S T A).symm‖ ≤ 1

The inverse of the splitting sumPiEquivProdPi has operator norm at most 1.

theorem ContinuousLinearEquiv.norm_symm_apply_le_inv_sqrt_mul_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E ≃L[𝕜] F) {lam : ℝ} (hlam : 0 < lam) (h : ∀ (y : E), lam * ‖y‖ ^ 2 ≤ ‖e y‖ ^ 2) (x : F) : ‖e.symm x‖ ≤ (√lam)⁻¹ * ‖x‖

A quadratic lower bound λ ‖y‖ ^ 2 ≤ ‖e y‖ ^ 2 with 0 < λ on a continuous linear equivalence e bounds its inverse: ‖e⁻¹ x‖ ≤ ‖x‖ / √λ.