Commit 2021-10-06 08:03 b534feda

refactor(analysis/{normed_space, inner_product_space}/dual): redefine using linear_isometry (#9569) Linear isometric embeddings appear naturally when studying the duals of normed spaces: the map λ y, ⟪x, y⟫ from an inner product space to its dual is a linear isometric embedding++, and so is the canonical map from a normed space to its double dual**. When these natural maps were defined last year, we didn't have the definition linear_isometry (notation: X →ₗᵢ[R] Y), so they were defined as continuous linear maps which satisfied the predicate isometry, and several lemmas were proven ad-hoc which are now available as general lemmas about linear_isometry. This PR refactors to use the linear_isometry structure. Lemmas deleted (I have been enthusiastic here, and can scale back if desired ...): normed_space.inclusion_in_double_dual_isometry inner_product_space.to_dual_map_isometry inner_product_space.to_dual_map_injective inner_product_space.ker_to_dual_map inner_product_space.to_dual_map_eq_iff_eq inner_product_space.range_to_dual_map inner_product_space.isometric.to_dual inner_product_space.to_dual_eq_iff_eq inner_product_space.to_dual_eq_iff_eq' inner_product_space.norm_to_dual_apply inner_product_space.norm_to_dual_symm_apply ++ (over ℝ -- over ℂ it's conjugate-linear, which will be dealt with in future PRs) ** over ℝ or ℂ