0_le_re_iner_orthogonalProjection

Stream: Is there code for X?

[Iván Renison]

Hi, do we have code for this?

variable {𝕜 E : Type*} [RCLike 𝕜]
variable? [HilbertSpace 𝕜 E] => [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
variable [FiniteDimensional 𝕜 E]

lemma zero_le_re_iner_orthogonalProjection (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E) :
    0 ≤ RCLike.re (inner 𝕜 (↑(K.orthogonalProjection x)) x) := sorry

My intuition for way this is true is very geometric, so I'm not being able to prove it, and I don't find it in Mathlib

[Jireh Loreaux]

My guess is probably not. What we should have (at some point, but do not currently I believe) is the map K.orthogonalProjection (which has type E →ₗ[𝕜] ↥K) as a map P : E →ₗ[𝕜] E, which is P := K.subtype ∘ₗ K.orthogonalProjection. This is a projection in the sense that P = P ^ 2 = star P, from which the result follows trivially (and we should develop API to make this so).

However, at this point, I don't think P is an existing definition in Mathlib, nor do we have any API developed for elements of the form P = P ^ 2 = star P.

[Iván Renison]

Ok, thanks

[Jireh Loreaux]

(side note: this lemma would be called re_inner_orthogonalProjection_nonneg or something, not zero_le...)

[Yury G. Kudryashov]

IMHO, the right lemma here is to say that this inner product is equal to the square of the norm of the projection.

[Iván Renison]

Great! With that idea I was able to prove it, and even to prove that it is a projection in the sense that P = P ^ 2 = star P. Thanks