@[simp]

theorem forall_mem_span_singleton {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (P : M → Prop) (u : M) : (∀ x ∈ R ∙ u, P x) ↔ ∀ (t : R), P (t • u)

@[simp]

theorem Field.exists_unit {𝕜 : Type u_1} [Field 𝕜] (P : 𝕜 → Prop) : (∃ (u : 𝕜ˣ), P ↑u) ↔ ∃ (u : 𝕜), u ≠ 0 ∧ P u

theorem span_singleton_eq_span_singleton_of_ne {𝕜 : Type u_1} [Field 𝕜] {M : Type u_2} [AddCommGroup M] [Module 𝕜 M] {u v : M} (hu : u ≠ 0) (hu' : u ∈ 𝕜 ∙ v) : 𝕜 ∙ u = 𝕜 ∙ v

@[reducible]

def spanLine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : Submodule ℝ E

The line (one-dimensional submodule of E) spanned by x : E.

Equations

• spanLine x = ℝ ∙ x

@[reducible]

noncomputable def spanOrthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : Submodule ℝ E

The orthogonal complement of the line spanned by x : E.

Equations

• spanOrthogonal x = (spanLine x)ᗮ

@[reducible]

noncomputable def projSpanOrthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : E →L[ℝ] ↥(ℝ ∙ x)ᗮ

The orthogonal projection to the complement of span x.

Equations

• projSpanOrthogonal x = (ℝ ∙ x)ᗮ.orthogonalProjectionOnto

theorem orthogonal_line_inf {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u v : E} : spanOrthogonal u ⊓ spanOrthogonal v = spanOrthogonal ↑((projSpanOrthogonal v) u) ⊓ spanOrthogonal v

theorem orthogonal_line_inf_sup_line {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u v : E) : spanOrthogonal u ⊓ spanOrthogonal v ⊔ spanLine ↑((projSpanOrthogonal v) u) = spanOrthogonal v

theorem orthogonalProjection_eq_zero_of_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Submodule ℝ E} [CompleteSpace ↥F] {x : E} (h : x ∈ Fᗮ) : F.orthogonalProjectionOnto x = 0

theorem inner_projection_self_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Submodule ℝ E} [CompleteSpace ↥F] {x : E} : inner ℝ x ↑(F.orthogonalProjectionOnto x) = 0 ↔ x ∈ Fᗮ

@[simp]

theorem mem_orthogonal_span_singleton_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x₀ x : E} : x ∈ spanOrthogonal x₀ ↔ inner ℝ x₀ x = 0

@[simp]

theorem orthogonalProjection_orthogonal_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y : E} : (projSpanOrthogonal x) y = ⟨y - (inner ℝ x y / inner ℝ x x) • x, ⋯⟩

theorem coe_orthogonalProjection_orthogonal_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y : E} : ↑((projSpanOrthogonal x) y) = y - (inner ℝ x y / inner ℝ x x) • x

theorem foo {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x₀ x : E} (h : inner ℝ x₀ x ≠ 0) (y : E) (hy : y ∈ spanOrthogonal x₀) : ↑((projSpanOrthogonal x) y) - (inner ℝ x₀ ↑((projSpanOrthogonal x) y) / inner ℝ x₀ x) • x = y

noncomputable def orthogonalProjectionOrthogonalLineIso {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x₀ x : E} (h : inner ℝ x₀ x ≠ 0) : ↥(spanOrthogonal x₀) ≃L[ℝ] ↥(spanOrthogonal x)

Given two non-orthogonal vectors in an inner product space, orthogonal_projection_orthogonal_line_iso is the continuous linear equivalence between their orthogonal complements obtained from orthogonal projection.

Equations

• One or more equations did not get rendered due to their size.

theorem orthogonalProjection_comp_coe {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) [CompleteSpace ↥K] : ⇑K.orthogonalProjectionOnto ∘ Subtype.val = id

theorem NormedSpace.continuousAt_iff {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (f : E → F) (x : E) : ContinuousAt f x ↔ ∀ ε > 0, ∃ δ > 0, ∀ (y : E), ‖y - x‖ < δ → ‖f y - f x‖ < ε

theorem NormedSpace.continuousAt_iff' {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (f : E → F) (x : E) : ContinuousAt f x ↔ ∀ ε > 0, ∃ δ > 0, ∀ (y : E), ‖y - x‖ ≤ δ → ‖f y - f x‖ ≤ ε

theorem NormedSpace.continuous_iff {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (f : E → F) : Continuous f ↔ ∀ (x : E), ∀ ε > 0, ∃ δ > 0, ∀ (y : E), ‖y - x‖ < δ → ‖f y - f x‖ < ε

theorem NormedSpace.continuous_iff' {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (f : E → F) : Continuous f ↔ ∀ (x : E), ∀ ε > 0, ∃ δ > 0, ∀ (y : E), ‖y - x‖ ≤ δ → ‖f y - f x‖ ≤ ε

theorem continuousAt_orthogonalProjection_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x₀ : E} (hx₀ : x₀ ≠ 0) : ContinuousAt (fun (x : E) => (spanOrthogonal x).subtypeL ∘SL projSpanOrthogonal x) x₀