Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-05 20:33 7cf0a29d

View on Github →

feat(analysis/normed_space/inner_product): consequences of characterization of orthogonal projection (#5558) Reverse order of equality in the lemma eq_orthogonal_projection_of_mem_of_inner_eq_zero. Add some variants. Also add three consequences:

the orthogonal projection onto K of an element of K is itself
the orthogonal projection onto K of an element of Kᗮ is zero
for a submodule K of an inner product space, the sum of the orthogonal projections onto K and Kᗮ is the identity. Reverse order of iff in the lemma submodule.eq_top_iff_orthogonal_eq_bot, and rename to submodule.orthogonal_eq_bot_iff.

Estimated changes

Modified src/analysis/normed_space/dual.lean

Modified src/analysis/normed_space/inner_product.lean

modified theorem eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero

modified theorem eq_orthogonal_projection_of_eq_submodule

modified theorem eq_orthogonal_projection_of_mem_of_inner_eq_zero

added theorem eq_orthogonal_projection_of_mem_orthogonal'

added theorem eq_orthogonal_projection_of_mem_orthogonal

added theorem eq_sum_orthogonal_projection_self_orthogonal_complement

modified theorem exists_norm_eq_infi_of_complete_subspace

added theorem id_eq_sum_orthogonal_projection_self_orthogonal_complement

modified theorem norm_eq_infi_iff_inner_eq_zero

modified theorem norm_eq_infi_iff_real_inner_eq_zero

modified theorem orthogonal_eq_inter

modified def orthogonal_projection

modified def orthogonal_projection_fn

modified theorem orthogonal_projection_fn_eq

modified theorem orthogonal_projection_fn_inner_eq_zero

modified theorem orthogonal_projection_fn_mem

modified theorem orthogonal_projection_fn_norm_sq

modified theorem orthogonal_projection_inner_eq_zero

added theorem orthogonal_projection_mem_subspace_eq_self

added theorem orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero

added theorem orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero

modified theorem orthogonal_projection_norm_le

deleted theorem submodule.eq_top_iff_orthogonal_eq_bot

modified theorem submodule.exists_sum_mem_mem_orthogonal

modified theorem submodule.inner_left_of_mem_orthogonal

modified theorem submodule.inner_right_of_mem_orthogonal

modified theorem submodule.is_closed_orthogonal

modified theorem submodule.is_compl_orthogonal_of_is_complete

modified theorem submodule.le_orthogonal_orthogonal

modified theorem submodule.mem_orthogonal'

modified theorem submodule.mem_orthogonal

modified def submodule.orthogonal

modified theorem submodule.orthogonal_disjoint

added theorem submodule.orthogonal_eq_bot_iff

added theorem submodule.orthogonal_eq_top_iff

modified theorem submodule.orthogonal_orthogonal

modified theorem submodule.sup_orthogonal_of_complete_space

modified theorem submodule.sup_orthogonal_of_is_complete

Modified src/analysis/normed_space/operator_norm.lean

added def submodule.subtype_continuous

added theorem submodule.subtype_continuous_apply