theorem eq_zero_of_mem_disjoint {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {F G : Submodule R M} (h : F ⊓ G = ⊥) {x : M} (hx : x ∈ F) (hx' : x ∈ G) : x = 0

@[simp]

theorem forall_mem_span_singleton {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (P : M → Prop) (u : M) : (∀ x ∈ Submodule.span 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 ∈ Submodule.span 𝕜 {v}) : Submodule.span 𝕜 {u} = Submodule.span 𝕜 {v}

theorem LinearIsometryEquiv.apply_ne_zero {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : E ≃ₗᵢ⋆[ℝ] F) {x : E} (hx : x ≠ 0) : φ x ≠ 0

@[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 = Submodule.span ℝ {x}

@[reducible]

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]

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

The orthogonal projection to the complement of span x.

Equations

• projSpanOrthogonal x = orthogonalProjection (Submodule.span ℝ {x})ᗮ

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ᗮ) : (orthogonalProjection F) 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 ↑((orthogonalProjection F) 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

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] : ⇑(orthogonalProjection K) ∘ 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.comp (projSpanOrthogonal x)) x₀