Documentation

Mathlib.Analysis.InnerProductSpace.Affine

Normed affine spaces over an inner product space #

source
theorem inner_vsub_left_eq_zero_symm {š•œ : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike š•œ] [NormedAddCommGroup V] [InnerProductSpace š•œ V] [MetricSpace P] [NormedAddTorsor V P] {a b : P} {v : V} :
inner š•œ (a -įµ„ b) v = 0 ā†” inner š•œ (b -įµ„ a) v = 0
source
theorem inner_vsub_right_eq_zero_symm {š•œ : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike š•œ] [NormedAddCommGroup V] [InnerProductSpace š•œ V] [MetricSpace P] [NormedAddTorsor V P] {v : V} {a b : P} :
inner š•œ v (a -įµ„ b) = 0 ā†” inner š•œ v (b -įµ„ a) = 0

In this section, the first left/right indicates where the common argument to vsub is, and the section refers to the argument of inner that ends up in the dist.

The lemma shapes are such that the relevant argument of inner remains unchanged, and that the other vsub preserves the position of the unchanging argument.

source
theorem inner_vsub_vsub_left_eq_dist_sq_left_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} :
inner ā„ (a -įµ„ b) (a -įµ„ c) = dist a b ^ 2 ā†” inner ā„ (a -įµ„ b) (b -įµ„ c) = 0
source
theorem inner_vsub_vsub_left_eq_dist_sq_right_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} :
inner ā„ (a -įµ„ b) (a -įµ„ c) = dist a c ^ 2 ā†” inner ā„ (c -įµ„ b) (a -įµ„ c) = 0
source
theorem inner_vsub_vsub_right_eq_dist_sq_left_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} :
inner ā„ (a -įµ„ c) (b -įµ„ c) = dist a c ^ 2 ā†” inner ā„ (a -įµ„ c) (b -įµ„ a) = 0
source
theorem inner_vsub_vsub_right_eq_dist_sq_right_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} :
inner ā„ (a -įµ„ c) (b -įµ„ c) = dist b c ^ 2 ā†” inner ā„ (a -įµ„ b) (b -įµ„ c) = 0
source
theorem dist_sq_lineMap_lineMap_of_inner_eq_zero {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} (tā‚ tā‚‚ : ā„) (h_inner : inner ā„ (b -įµ„ a) (c -įµ„ a) = 0) :
dist ((AffineMap.lineMap a b) tā‚) ((AffineMap.lineMap a c) tā‚‚) ^ 2 = tā‚ ^ 2 * dist a b ^ 2 + tā‚‚ ^ 2 * dist a c ^ 2

Squared distance between two points on lines from a common origin, given orthogonality of the direction vectors.

source
theorem dist_sq_lineMap_of_inner_eq_zero {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] {a b p : P} (t : ā„) (h_inner : inner ā„ (p -įµ„ a) (b -įµ„ a) = 0) :
dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2

Squared distance from p to a point on the line from a to b, given that p -įµ„ a is orthogonal to b -įµ„ a.

source
theorem dist_sq_of_inner_eq_zero {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] {a b p : P} (h_inner : inner ā„ (p -įµ„ a) (b -įµ„ a) = 0) :
dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2

Pythagorean theorem: if p -įµ„ a is orthogonal to b -įµ„ a, then dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2.