Conformal Linear Maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A continuous linear map between R-normed spaces X and Y is_conformal_map if it is
a nonzero multiple of a linear isometry.
Main definitions #
is_conformal_map: the main definition of conformal linear maps
Main results #
- The conformality of the composition of two conformal linear maps, the identity map and multiplications by nonzero constants as continuous linear maps
is_conformal_map_of_subsingleton: all continuous linear maps on singleton spaces are conformalis_conformal_map.preserves_angle: if a continuous linear map is conformal, then it preserves all angles in the normed space
See analysis.normed_space.conformal_linear_map.inner_product for
is_conformal_map_iff: a map between inner product spaces is conformal iff it preserves inner products up to a fixed scalar factor.
Tags #
conformal
Warning #
The definition of conformality in this file does NOT require the maps to be orientation-preserving.
def
is_conformal_map
{R : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[normed_field R]
[seminormed_add_comm_group X]
[seminormed_add_comm_group Y]
[normed_space R X]
[normed_space R Y]
(f' : X →L[R] Y) :
Prop
A continuous linear map f' is said to be conformal if it's
a nonzero multiple of a linear isometry.
Equations
- is_conformal_map f' = ∃ (c : R) (hc : c ≠ 0) (li : X →ₗᵢ[R] Y), f' = c • li.to_continuous_linear_map
theorem
is_conformal_map_id
{R : Type u_1}
{M : Type u_2}
[normed_field R]
[seminormed_add_comm_group M]
[normed_space R M] :
theorem
is_conformal_map.smul
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[normed_field R]
[seminormed_add_comm_group M]
[seminormed_add_comm_group N]
[normed_space R M]
[normed_space R N]
{f : M →L[R] N}
(hf : is_conformal_map f)
{c : R}
(hc : c ≠ 0) :
is_conformal_map (c • f)
theorem
is_conformal_map_const_smul
{R : Type u_1}
{M : Type u_2}
[normed_field R]
[seminormed_add_comm_group M]
[normed_space R M]
{c : R}
(hc : c ≠ 0) :
@[protected]
theorem
linear_isometry.is_conformal_map
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[normed_field R]
[seminormed_add_comm_group M]
[seminormed_add_comm_group N]
[normed_space R M]
[normed_space R N]
(f' : M →ₗᵢ[R] N) :
theorem
is_conformal_map_of_subsingleton
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[normed_field R]
[seminormed_add_comm_group M]
[seminormed_add_comm_group N]
[normed_space R M]
[normed_space R N]
[subsingleton M]
(f' : M →L[R] N) :
theorem
is_conformal_map.comp
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{G : Type u_4}
[normed_field R]
[seminormed_add_comm_group M]
[seminormed_add_comm_group N]
[seminormed_add_comm_group G]
[normed_space R M]
[normed_space R N]
[normed_space R G]
{f : M →L[R] N}
{g : N →L[R] G}
(hg : is_conformal_map g)
(hf : is_conformal_map f) :
is_conformal_map (g.comp f)
@[protected]
theorem
is_conformal_map.injective
{R : Type u_1}
{N : Type u_3}
{M' : Type u_5}
[normed_field R]
[seminormed_add_comm_group N]
[normed_space R N]
[normed_add_comm_group M']
[normed_space R M']
{f : M' →L[R] N}
(h : is_conformal_map f) :
theorem
is_conformal_map.ne_zero
{R : Type u_1}
{N : Type u_3}
{M' : Type u_5}
[normed_field R]
[seminormed_add_comm_group N]
[normed_space R N]
[normed_add_comm_group M']
[normed_space R M']
[nontrivial M']
{f' : M' →L[R] N}
(hf' : is_conformal_map f') :
f' ≠ 0