English
A restatement of uniqueness: if u,v ∈ E satisfy the orthogonality condition with all w ∈ K, then the unbundled projection of u equals v.
Русский
Утверждение об уникальности: если для всех w∈K верно ⟪u−v, w⟫ = 0, то K.orthogonalProjectionFn(u) = v.
LaTeX
$$$\forall w∈K, \langle u-v, w\rangle = 0 \Rightarrow K.orthogonalProjectionFn(u) = v$$$
Lean4
/-- The orthogonal projection onto a complete subspace. -/
def orthogonalProjection : E →L[𝕜] K :=
LinearMap.mkContinuous
{ toFun := fun v => ⟨K.orthogonalProjectionFn v, orthogonalProjectionFn_mem v⟩
map_add' := fun x y =>
by
have hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K :=
Submodule.add_mem K (orthogonalProjectionFn_mem x) (orthogonalProjectionFn_mem y)
have ho : ∀ w ∈ K, ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0 :=
by
intro w hw
rw [add_sub_add_comm, inner_add_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
orthogonalProjectionFn_inner_eq_zero _ w hw, add_zero]
ext
simp [eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hm ho]
map_smul' := fun c x =>
by
have hm : c • K.orthogonalProjectionFn x ∈ K := Submodule.smul_mem K _ (orthogonalProjectionFn_mem x)
have ho : ∀ w ∈ K, ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0 :=
by
intro w hw
rw [← smul_sub, inner_smul_left, orthogonalProjectionFn_inner_eq_zero _ w hw, mul_zero]
ext
simp [eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hm ho] }
1 fun x => by
simp only [one_mul, LinearMap.coe_mk]
refine le_of_pow_le_pow_left₀ two_ne_zero (norm_nonneg _) ?_
change ‖K.orthogonalProjectionFn x‖ ^ 2 ≤ ‖x‖ ^ 2
nlinarith [K.orthogonalProjectionFn_norm_sq x]
