def euclideanDist (n : ℕ) (x y : EuclideanSpace ℝ (Fin n)) : ℝ

Text 6.1: The Euclidean distance between two points x and y in R^n is defined by d(x, y) = |x - y| = sqrt (inner (x - y) (x - y)).

Equations

• euclideanDist n x y = dist x y

theorem convexOn_univ_norm_comp_sub (n : ℕ) : ConvexOn ℝ Set.univ fun (p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) => ‖p.1 - p.2‖

The norm of the difference on a product space is convex on all of R^{2n}.

theorem euclideanDist_convex (n : ℕ) : ConvexOn ℝ Set.univ fun (p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) => dist p.1 p.2

Text 6.2: The function d, the Euclidean metric, is convex as a function on R^{2n}.

def euclideanUnitBall (n : ℕ) : Set (EuclideanSpace ℝ (Fin n))

Text 6.3: Throughout this section, the Euclidean unit ball in R^n is B = {x | ‖x‖ ≤ 1} = {x | dist x 0 ≤ 1}.

Equations

• euclideanUnitBall n = {x : EuclideanSpace ℝ (Fin n) | ‖x‖ ≤ 1}

theorem euclideanUnitBall_eq_dist (n : ℕ) : euclideanUnitBall n = {x : EuclideanSpace ℝ (Fin n) | dist x 0 ≤ 1}

theorem euclideanUnitBall_closed_convex (n : ℕ) : IsClosed (euclideanUnitBall n) ∧ Convex ℝ (euclideanUnitBall n)

Text 6.4: The Euclidean unit ball B is a closed convex set.

theorem euclidean_closedBall_eq_translate_left (n : ℕ) (a : EuclideanSpace ℝ (Fin n)) (ε : ℝ) : {x : EuclideanSpace ℝ (Fin n) | dist x a ≤ ε} = (fun (y : EuclideanSpace ℝ (Fin n)) => a + y) '' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ≤ ε}

Text 6.5: For any a ∈ R^n, the ball with radius ε > 0 and center a is {x | d(x, a) ≤ ε} = {a + y | |y| ≤ ε} = a + ε B. The closed ball centered at a is a translate of the radius-ε norm ball.

theorem euclidean_normBall_eq_smul_unitBall (n : ℕ) (ε : ℝ) (hε : 0 ≤ ε) : {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ≤ ε} = ε • euclideanUnitBall n

Scaling the unit ball by ε ≥ 0 gives the radius-ε norm ball.

theorem image_translate_smul_unitBall (n : ℕ) (a : EuclideanSpace ℝ (Fin n)) (ε : ℝ) : (fun (y : EuclideanSpace ℝ (Fin n)) => a + y) '' (ε • euclideanUnitBall n) = (fun (y : EuclideanSpace ℝ (Fin n)) => a + ε • y) '' euclideanUnitBall n

Translating the ε-scaled unit ball equals scaling after translating.

theorem euclidean_closedBall_eq_translate (n : ℕ) (a : EuclideanSpace ℝ (Fin n)) (ε : ℝ) (hε : 0 < ε) : {x : EuclideanSpace ℝ (Fin n) | dist x a ≤ ε} = (fun (y : EuclideanSpace ℝ (Fin n)) => a + y) '' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ≤ ε} ∧ (fun (y : EuclideanSpace ℝ (Fin n)) => a + y) '' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ≤ ε} = (fun (y : EuclideanSpace ℝ (Fin n)) => a + ε • y) '' euclideanUnitBall n

theorem euclidean_neighborhood_eq_iUnion_translate (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (ε : ℝ) (hε : 0 ≤ ε) : {x : EuclideanSpace ℝ (Fin n) | ∃ y ∈ C, dist x y ≤ ε} = ⋃ y ∈ C, (fun (z : EuclideanSpace ℝ (Fin n)) => y + z) '' (ε • euclideanUnitBall n) ∧ ⋃ y ∈ C, (fun (z : EuclideanSpace ℝ (Fin n)) => y + z) '' (ε • euclideanUnitBall n) = C + ε • euclideanUnitBall n

Text 6.6: For any set C in R^n, the set of points x whose distance from C does not exceed ε is {x | ∃ y ∈ C, d(x, y) ≤ ε} = ⋃ {y + ε B | y ∈ C} = C + ε B.

theorem euclidean_closure_eq_iInter_thickening (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : closure C = ⋂ (ε : { ε : ℝ // 0 < ε }), C + ↑ε • euclideanUnitBall n

Text 6.7: The closure cl C of C can be expressed by cl C = ⋂ { C + ε B | ε > 0 }.

theorem euclidean_interior_eq_setOf_exists_thickening (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : interior C = {x : EuclideanSpace ℝ (Fin n) | ∃ (ε : ℝ), 0 < ε ∧ (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' (ε • euclideanUnitBall n) ⊆ C}

Text 6.7: The interior int C of C can be expressed by int C = { x | ∃ ε > 0, x + ε B ⊆ C }.

def euclideanRelativeInterior (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : Set (EuclideanSpace ℝ (Fin n))

Text 6.8: The relative interior ri C of a convex set C in R^n is the interior of C in its affine hull aff C. Equivalently, ri C = { x ∈ aff C | ∃ ε > 0, (x + ε B) ∩ aff C ⊆ C }.

Equations

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

theorem euclideanRelativeInterior_subset_closure (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : euclideanRelativeInterior n C ⊆ C ∧ C ⊆ closure C

Text 6.9: Needless to say, ri C ⊂ C ⊂ cl C.

def euclideanRelativeBoundary (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : Set (EuclideanSpace ℝ (Fin n))

Text 6.10: The relative boundary of C is the set difference (cl C) \ (ri C).

Equations

• euclideanRelativeBoundary n C = closure C \ euclideanRelativeInterior n C

def euclideanRelativelyOpen (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : Prop

Text 6.11: Naturally, C is said to be relatively open if ri C = C.

Equations

• euclideanRelativelyOpen n C = (euclideanRelativeInterior n C = C)

theorem euclideanRelativeInterior_eq_interior_of_affineSpan_eq_univ (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : ↑(affineSpan ℝ C) = Set.univ) : euclideanRelativeInterior n C = interior C

Text 6.12: For an n-dimensional convex set, aff C = R^n by definition, so ri C = int C.

theorem euclideanRelativeInterior_affineSubspace_eq (n : ℕ) (s : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) : euclideanRelativeInterior n ↑s = ↑s

The relative interior of an affine subspace is the subspace itself.

theorem affineSubspace_isClosed (n : ℕ) (s : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) : IsClosed ↑s

Every affine subspace of Euclidean space is closed.

theorem affineSubspace_relativelyOpen_closed (n : ℕ) (s : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) : euclideanRelativelyOpen n ↑s ∧ IsClosed ↑s

Text 6.13: An affine set is relatively open by definition. Every affine set is at the same time closed.

theorem euclidean_closure_subset_closure_affineSpan (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : closure C ⊆ closure ↑(affineSpan ℝ C) ∧ closure ↑(affineSpan ℝ C) = ↑(affineSpan ℝ C)

Text 6.14: Observe that cl C ⊆ cl (aff C) = aff C for any C.

theorem translate_smul_unitBall_eq_closedBall (n : ℕ) (a : EuclideanSpace ℝ (Fin n)) (ε : ℝ) (hε : 0 < ε) : (fun (y : EuclideanSpace ℝ (Fin n)) => a + y) '' (ε • euclideanUnitBall n) = Metric.closedBall a ε

The translated scaled unit ball is the metric closed ball.

theorem closure_image_affineEquiv (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (e : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) : closure (⇑e '' C) = ⇑e '' closure C

Text 6.15: Closures and relative interiors are preserved under translations and, more generally, under any one-to-one affine transformation of R^n onto itself. Such maps preserve affine hulls and are continuous in both directions.

theorem affineSpan_image_affineEquiv (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (e : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) : ⇑e '' ↑(affineSpan ℝ C) = ↑(affineSpan ℝ (⇑e '' C))

Affine equivalences send affine spans to affine spans of the images.

theorem affineEquiv_symm_image_image (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (e : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) : ⇑e.symm '' (⇑e '' C) = C

The inverse affine equivalence cancels the direct image of a set.

theorem ri_image_affineEquiv_subset (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (e : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) : ⇑e '' euclideanRelativeInterior n C ⊆ euclideanRelativeInterior n (⇑e '' C)

An affine equivalence sends relative interior into relative interior.

theorem euclideanRelativeInterior_image_affineEquiv (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (e : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) : euclideanRelativeInterior n (⇑e '' C) = ⇑e '' euclideanRelativeInterior n C

Text 6.15: Relative interiors are preserved under one-to-one affine transformations of R^n onto itself (hence in particular under translations).

def coordinateSubspace (n m : ℕ) : Set (EuclideanSpace ℝ (Fin n))

The coordinate subspace where coordinates m, ..., n-1 vanish.

Equations

• coordinateSubspace n m = {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), m ≤ ↑i → x.ofLp i = 0}

@[simp]

theorem piCongrLeft_apply_const {ι : Type u_1} {ι' : Type u_2} (e : ι' ≃ ι) (f : ι' → ℝ) (i : ι) : (LinearEquiv.piCongrLeft ℝ (fun (x : ι) => ℝ) e) f i = f (e.symm i)

Evaluate LinearEquiv.piCongrLeft on a constant codomain.

@[simp]

theorem piCongrLeft_symm_apply_const {ι : Type u_1} {ι' : Type u_2} (e : ι' ≃ ι) (f : ι → ℝ) (i : ι') : (LinearEquiv.piCongrLeft ℝ (fun (x : ι) => ℝ) e).symm f i = f (e i)

Evaluate the inverse of LinearEquiv.piCongrLeft on a constant codomain.

theorem exists_affineEquiv_affineSpan_eq_coordinateSubspace (n m : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hCnonempty : C.Nonempty) (hCdim : Module.finrank ℝ ↥(affineSpan ℝ C).direction = m) : ∃ (T : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n)), ⇑T '' ↑(affineSpan ℝ C) = coordinateSubspace n m

Text 6.16: For example, if C is an m-dimensional convex set in R^n, there exists by Corollary 1.6.1 a one-to-one affine transformation T of R^n onto itself which carries aff C onto the subspace L = { x = (xi_1, ..., xi_n) | xi_{m+1} = 0, ..., xi_n = 0 }. This L can be regarded as a copy of R^m.

theorem translate_smul_unitBall_subset_translate_smul_unitBall (n : ℕ) {x y : EuclideanSpace ℝ (Fin n)} {ε : ℝ} (hε : 0 < ε) (hy : y ∈ (fun (v : EuclideanSpace ℝ (Fin n)) => x + v) '' ((ε / 2) • euclideanUnitBall n)) : (fun (v : EuclideanSpace ℝ (Fin n)) => y + v) '' ((ε / 2) • euclideanUnitBall n) ⊆ (fun (v : EuclideanSpace ℝ (Fin n)) => x + v) '' (ε • euclideanUnitBall n)

A half-radius translated ball around y stays inside the translated ball around x when y is within the half-radius ball around x.

theorem small_ball_subset_relativeInterior (n : ℕ) {C : Set (EuclideanSpace ℝ (Fin n))} {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n C) : ∃ (ε : ℝ), 0 < ε ∧ (fun (y : EuclideanSpace ℝ (Fin n)) => x + y) '' ((ε / 2) • euclideanUnitBall n) ∩ ↑(affineSpan ℝ C) ⊆ euclideanRelativeInterior n C

A half-radius relative ball around a relative interior point is still in the relative interior.

theorem euclidean_closure_closure_eq_and_relativeInterior_relativeInterior_eq (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) : closure (closure C) = closure C ∧ euclideanRelativeInterior n (euclideanRelativeInterior n C) = euclideanRelativeInterior n C

Text 6.17: For any set C in R^n, convex or not, the laws cl (cl C) = cl C and ri (ri C) = ri C are valid.

def directSumSetEuclidean (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : Set (EuclideanSpace ℝ (Fin (m + p)))

Auxiliary: the direct-sum set C1 ⊕ C2 in R^{m+p}, built via Fin.appendIsometry.

Equations

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

theorem directSumSetEuclidean_eq_image_append (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : have append := fun (x : EuclideanSpace ℝ (Fin m)) (y : EuclideanSpace ℝ (Fin p)) => (EuclideanSpace.equiv (Fin (m + p)) ℝ).symm ((Fin.appendIsometry m p) ((EuclideanSpace.equiv (Fin m) ℝ) x, (EuclideanSpace.equiv (Fin p) ℝ) y)); directSumSetEuclidean m p C1 C2 = (fun (xy : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin p)) => append xy.1 xy.2) '' C1.prod C2

Express the direct-sum set as the image of the product under the append map.

noncomputable def appendHomeomorph (m p : ℕ) : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin p) ≃ₜ EuclideanSpace ℝ (Fin (m + p))

The append map on Euclidean spaces is a homeomorphism.

Equations

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

noncomputable def appendAffineEquiv (m p : ℕ) : EuclideanSpace ℝ (Fin m) × EuclideanSpace ℝ (Fin p) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin (m + p))

The append map on Euclidean spaces is an affine equivalence.

Equations

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

theorem appendAffineEquiv_apply (m p : ℕ) (x : EuclideanSpace ℝ (Fin m)) (y : EuclideanSpace ℝ (Fin p)) : (appendAffineEquiv m p) (x, y) = (EuclideanSpace.equiv (Fin (m + p)) ℝ).symm ((Fin.appendIsometry m p) ((EuclideanSpace.equiv (Fin m) ℝ) x, (EuclideanSpace.equiv (Fin p) ℝ) y))

The append affine equivalence acts as the explicit append map on coordinates.

theorem directSumSetEuclidean_eq_image_appendAffineEquiv (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : directSumSetEuclidean m p C1 C2 = ⇑(appendAffineEquiv m p) '' C1.prod C2

Express the direct-sum set as the image of the product under appendAffineEquiv.

theorem affineSpan_prod_eq (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : ↑(affineSpan ℝ (C1.prod C2)) = (↑(affineSpan ℝ C1)).prod ↑(affineSpan ℝ C2)

The affine span of a product is the product of affine spans.

theorem affineSpan_directSumSetEuclidean_eq (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : ↑(affineSpan ℝ (directSumSetEuclidean m p C1 C2)) = directSumSetEuclidean m p ↑(affineSpan ℝ C1) ↑(affineSpan ℝ C2)

The affine span of the direct-sum set factors as the direct sum of affine spans.

theorem closure_directSumSetEuclidean_eq (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : closure (directSumSetEuclidean m p C1 C2) = directSumSetEuclidean m p (closure C1) (closure C2)

The closure of the direct-sum set factors as the direct sum of closures.

theorem euclideanRelativeInterior_directSumSetEuclidean_subset (m p : ℕ) (C1 : Set (EuclideanSpace ℝ (Fin m))) (C2 : Set (EuclideanSpace ℝ (Fin p))) : euclideanRelativeInterior (m + p) (directSumSetEuclidean m p C1 C2) ⊆ directSumSetEuclidean m p (euclideanRelativeInterior m C1) (euclideanRelativeInterior p C2)

Forward inclusion for the relative interior of a direct sum.