Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Source-normalized coordinate cubes

This file records the cube notation used in the source proof. The normalized theorem is first proved on Q 3 = (-3, 3)^n with conclusion on Q 1 = (-1, 1)^n.

@[reducible, inline]

abbrev AleksandrovDifferentiability.SourceCubeSpace (n : ℕ) : Type

The source-proof coordinate space R^n, with its Euclidean inner-product structure.

Equations

• AleksandrovDifferentiability.SourceCubeSpace n = EuclideanSpace ℝ (Fin n)

def AleksandrovDifferentiability.sourceOpenCubeAt {n : ℕ} (c : SourceCubeSpace n) (r : ℝ) : Set (SourceCubeSpace n)

The translated open coordinate cube Q_r(c) = c + (-r, r)^n.

Equations

• AleksandrovDifferentiability.sourceOpenCubeAt c r = {x : AleksandrovDifferentiability.SourceCubeSpace n | ∀ (i : Fin n), |x.ofLp i - c.ofLp i| < r}

def AleksandrovDifferentiability.sourceOpenCube (n : ℕ) (r : ℝ) : Set (SourceCubeSpace n)

The centered open coordinate cube Q_r = (-r, r)^n.

Equations

• AleksandrovDifferentiability.sourceOpenCube n r = AleksandrovDifferentiability.sourceOpenCubeAt 0 r

def AleksandrovDifferentiability.sourceClosedCube (n : ℕ) (r : ℝ) : Set (SourceCubeSpace n)

The centered closed coordinate cube [-r, r]^n. It is mainly used as the compact set between Q_1 and Q_3 in the source-local differentiability-a.e. argument.

Equations

• AleksandrovDifferentiability.sourceClosedCube n r = {x : AleksandrovDifferentiability.SourceCubeSpace n | ∀ (i : Fin n), |x.ofLp i| ≤ r}

noncomputable def AleksandrovDifferentiability.oscOn {E : Type u_1} (u : E → ℝ) (s : Set E) : ℝ

The oscillation of a real-valued function on a set, written in the source as osc_s u. Later estimates carry boundedness and nonemptiness hypotheses when they need the usual order properties of sSup and sInf.

Equations

• AleksandrovDifferentiability.oscOn u s = sSup (u '' s) - sInf (u '' s)

def AleksandrovDifferentiability.BoundedOn {E : Type u_1} (s : Set E) (u : E → ℝ) : Prop

u is bounded on s in the bornological sense.

Equations

• AleksandrovDifferentiability.BoundedOn s u = Bornology.IsBounded (u '' s)

theorem AleksandrovDifferentiability.BoundedOn.mono {E : Type u_1} {s t : Set E} {u : E → ℝ} (h : BoundedOn t u) (hst : s ⊆ t) : BoundedOn s u

Boundedness on a larger set restricts to boundedness on a subset.

theorem AleksandrovDifferentiability.BoundedOn.of_isCompact_of_continuousOn {E : Type u_1} [TopologicalSpace E] {s : Set E} {u : E → ℝ} (hs : IsCompact s) (hu : ContinuousOn u s) : BoundedOn s u

A continuous real-valued function on a compact set is bounded in the project BoundedOn sense.

noncomputable def AleksandrovDifferentiability.sourceCoordinateVector {n : ℕ} (i : Fin n) : SourceCubeSpace n

The i-th Euclidean coordinate vector in the source cube model.

Equations

• AleksandrovDifferentiability.sourceCoordinateVector i = (EuclideanSpace.basisFun (Fin n) ℝ) i

noncomputable def AleksandrovDifferentiability.coordinateLineBase {n : ℕ} (i : Fin n) (x : SourceCubeSpace n) : SourceCubeSpace n

The base point of the coordinate line through x parallel to the i-th axis, obtained by zeroing the i-th coordinate.

Equations

• AleksandrovDifferentiability.coordinateLineBase i x = x - x.ofLp i • AleksandrovDifferentiability.sourceCoordinateVector i

noncomputable def AleksandrovDifferentiability.coordinateLinePoint {n : ℕ} (i : Fin n) (y : SourceCubeSpace n) (s : ℝ) : SourceCubeSpace n

The point y + s e_i on the coordinate line through y parallel to the i-th axis.

Equations

• AleksandrovDifferentiability.coordinateLinePoint i y s = y + s • AleksandrovDifferentiability.sourceCoordinateVector i

@[reducible, inline]

abbrev AleksandrovDifferentiability.SourceTransverseSpace {n : ℕ} (i : Fin n) : Type

The transverse coordinate space to the i-th source-coordinate direction.

Equations

• AleksandrovDifferentiability.SourceTransverseSpace i = EuclideanSpace ℝ { j : Fin n // j ≠ i }

def AleksandrovDifferentiability.sourceTransverseOpenCube {n : ℕ} (i : Fin n) (r : ℝ) : Set (SourceTransverseSpace i)

The open transverse cube in the coordinate hyperplane perpendicular to e_i.

Equations

• AleksandrovDifferentiability.sourceTransverseOpenCube i r = {a : AleksandrovDifferentiability.SourceTransverseSpace i | ∀ (j : { j : Fin n // j ≠ i }), |a.ofLp j| < r}

def AleksandrovDifferentiability.sourceTransverseEmbed {n : ℕ} (i : Fin n) (a : SourceTransverseSpace i) : SourceCubeSpace n

Embed transverse coordinates into the source cube by inserting zero in coordinate i.

Equations

• AleksandrovDifferentiability.sourceTransverseEmbed i a = WithLp.toLp 2 fun (j : Fin n) => if h : j = i then 0 else a.ofLp ⟨j, h⟩

noncomputable def AleksandrovDifferentiability.sourceCoordinateChartPoint {n : ℕ} (i : Fin n) (a : SourceTransverseSpace i) (s : ℝ) : SourceCubeSpace n

Product-coordinate chart for the i-th coordinate line: transverse base plus vertical coordinate.

Equations

• AleksandrovDifferentiability.sourceCoordinateChartPoint i a s = AleksandrovDifferentiability.sourceTransverseEmbed i a + s • AleksandrovDifferentiability.sourceCoordinateVector i

noncomputable def AleksandrovDifferentiability.sourceCoordinateChartMap {n : ℕ} (i : Fin n) : SourceTransverseSpace i × ℝ → SourceCubeSpace n

Product-coordinate chart map for the i-th source-coordinate direction.

Equations

• AleksandrovDifferentiability.sourceCoordinateChartMap i p = AleksandrovDifferentiability.sourceCoordinateChartPoint i p.1 p.2

@[simp]

theorem AleksandrovDifferentiability.mem_sourceOpenCubeAt {n : ℕ} {c x : SourceCubeSpace n} {r : ℝ} : x ∈ sourceOpenCubeAt c r ↔ ∀ (i : Fin n), |x.ofLp i - c.ofLp i| < r

@[simp]

theorem AleksandrovDifferentiability.mem_sourceOpenCube {n : ℕ} {x : SourceCubeSpace n} {r : ℝ} : x ∈ sourceOpenCube n r ↔ ∀ (i : Fin n), |x.ofLp i| < r

@[simp]

theorem AleksandrovDifferentiability.mem_sourceClosedCube {n : ℕ} {x : SourceCubeSpace n} {r : ℝ} : x ∈ sourceClosedCube n r ↔ ∀ (i : Fin n), |x.ofLp i| ≤ r

theorem AleksandrovDifferentiability.sourceOpenCubeAt_subset_of_le {n : ℕ} {c : SourceCubeSpace n} {r R : ℝ} (hrR : r ≤ R) : sourceOpenCubeAt c r ⊆ sourceOpenCubeAt c R

theorem AleksandrovDifferentiability.sourceOpenCube_subset_of_le {n : ℕ} {r R : ℝ} (hrR : r ≤ R) : sourceOpenCube n r ⊆ sourceOpenCube n R

theorem AleksandrovDifferentiability.sourceOpenCube_one_subset_three {n : ℕ} : sourceOpenCube n 1 ⊆ sourceOpenCube n 3

theorem AleksandrovDifferentiability.sourceOpenCube_subset_sourceClosedCube_of_le {n : ℕ} {r R : ℝ} (hrR : r ≤ R) : sourceOpenCube n r ⊆ sourceClosedCube n R

theorem AleksandrovDifferentiability.sourceOpenCube_one_subset_sourceClosedCube_one {n : ℕ} : sourceOpenCube n 1 ⊆ sourceClosedCube n 1

theorem AleksandrovDifferentiability.sourceClosedCube_subset_sourceOpenCube_of_lt {n : ℕ} {r R : ℝ} (hrR : r < R) : sourceClosedCube n r ⊆ sourceOpenCube n R

theorem AleksandrovDifferentiability.sourceClosedCube_one_subset_sourceOpenCube_three {n : ℕ} : sourceClosedCube n 1 ⊆ sourceOpenCube n 3

theorem AleksandrovDifferentiability.center_mem_sourceOpenCubeAt {n : ℕ} {c : SourceCubeSpace n} {r : ℝ} (hr : 0 < r) : c ∈ sourceOpenCubeAt c r

theorem AleksandrovDifferentiability.zero_mem_sourceOpenCube {n : ℕ} {r : ℝ} (hr : 0 < r) : 0 ∈ sourceOpenCube n r

theorem AleksandrovDifferentiability.sourceOpenCubeAt_eq_iInter {n : ℕ} (c : SourceCubeSpace n) (r : ℝ) : sourceOpenCubeAt c r = ⋂ (i : Fin n), {x : SourceCubeSpace n | |x.ofLp i - c.ofLp i| < r}

theorem AleksandrovDifferentiability.sourceClosedCube_eq_iInter {n : ℕ} (r : ℝ) : sourceClosedCube n r = ⋂ (i : Fin n), {x : SourceCubeSpace n | |x.ofLp i| ≤ r}

theorem AleksandrovDifferentiability.sourceTransverseOpenCube_eq_iInter {n : ℕ} (i : Fin n) (r : ℝ) : sourceTransverseOpenCube i r = ⋂ (j : { j : Fin n // j ≠ i }), {a : SourceTransverseSpace i | |a.ofLp j| < r}

theorem AleksandrovDifferentiability.isOpen_sourceOpenCubeAt {n : ℕ} (c : SourceCubeSpace n) (r : ℝ) : IsOpen (sourceOpenCubeAt c r)

theorem AleksandrovDifferentiability.isOpen_sourceOpenCube {n : ℕ} (r : ℝ) : IsOpen (sourceOpenCube n r)

theorem AleksandrovDifferentiability.convex_sourceOpenCubeAt {n : ℕ} (c : SourceCubeSpace n) (r : ℝ) : Convex ℝ (sourceOpenCubeAt c r)

Source open cubes are convex.

theorem AleksandrovDifferentiability.convex_sourceOpenCube {n : ℕ} (r : ℝ) : Convex ℝ (sourceOpenCube n r)

Centered source open cubes are convex.

theorem AleksandrovDifferentiability.isOpen_sourceTransverseOpenCube {n : ℕ} (i : Fin n) (r : ℝ) : IsOpen (sourceTransverseOpenCube i r)

theorem AleksandrovDifferentiability.continuous_sourceTransverseEmbed {n : ℕ} (i : Fin n) : Continuous (sourceTransverseEmbed i)

theorem AleksandrovDifferentiability.continuous_sourceCoordinateChartMap {n : ℕ} (i : Fin n) : Continuous (sourceCoordinateChartMap i)

theorem AleksandrovDifferentiability.continuous_coordinateLineBase {n : ℕ} (i : Fin n) : Continuous (coordinateLineBase i)

The coordinate-line base projection x ↦ x - x_i e_i is continuous.

theorem AleksandrovDifferentiability.isClosed_sourceClosedCube {n : ℕ} (r : ℝ) : IsClosed (sourceClosedCube n r)

theorem AleksandrovDifferentiability.isBounded_sourceClosedCube {n : ℕ} {r : ℝ} (hr : 0 ≤ r) : Bornology.IsBounded (sourceClosedCube n r)

theorem AleksandrovDifferentiability.norm_le_sqrt_card_mul_of_mem_sourceOpenCube {n : ℕ} {r : ℝ} (hr : 0 ≤ r) {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n r) : ‖x‖ ≤ √↑n * r

Explicit Euclidean norm bound for points in the source open cube.

theorem AleksandrovDifferentiability.isBounded_sourceTransverseOpenCube {n : ℕ} (i : Fin n) {r : ℝ} (hr : 0 ≤ r) : Bornology.IsBounded (sourceTransverseOpenCube i r)

The transverse open coordinate cube is bounded.

theorem AleksandrovDifferentiability.isCompact_sourceClosedCube {n : ℕ} {r : ℝ} (hr : 0 ≤ r) : IsCompact (sourceClosedCube n r)

theorem AleksandrovDifferentiability.BoundedOn.sourceOpenCube_of_continuousOn_sourceClosedCube {n : ℕ} {u : SourceCubeSpace n → ℝ} {r : ℝ} (hr : 0 ≤ r) (hcont : ContinuousOn u (sourceClosedCube n r)) : BoundedOn (sourceOpenCube n r) u

Continuity on the closed cube gives the boundedness hypothesis needed by the normalized source-cube theorem on the corresponding open cube.

theorem AleksandrovDifferentiability.sourceOpenCube_subset_interior_of_le {n : ℕ} {r R : ℝ} (hrR : r ≤ R) : sourceOpenCube n r ⊆ interior (sourceOpenCube n R)

Since source cubes are open, inclusion in a larger source cube also gives inclusion in its interior.

theorem AleksandrovDifferentiability.sourceOpenCube_one_subset_interior_three {n : ℕ} : sourceOpenCube n 1 ⊆ interior (sourceOpenCube n 3)

@[simp]

theorem AleksandrovDifferentiability.sourceCoordinateVector_apply_self {n : ℕ} (i : Fin n) : (sourceCoordinateVector i).ofLp i = 1

theorem AleksandrovDifferentiability.sourceCoordinateVector_apply_ne {n : ℕ} {i j : Fin n} (hji : j ≠ i) : (sourceCoordinateVector i).ofLp j = 0

@[simp]

theorem AleksandrovDifferentiability.norm_sourceCoordinateVector {n : ℕ} (i : Fin n) : ‖sourceCoordinateVector i‖ = 1

theorem AleksandrovDifferentiability.exists_unit_sourceCubeSpace_of_pos {n : ℕ} (hn : 0 < n) : ∃ (v : SourceCubeSpace n), ‖v‖ = 1

A positive-dimensional source cube space contains a unit vector.

@[simp]

theorem AleksandrovDifferentiability.coordinateLineBase_apply_self {n : ℕ} (i : Fin n) (x : SourceCubeSpace n) : (coordinateLineBase i x).ofLp i = 0

theorem AleksandrovDifferentiability.coordinateLineBase_apply_ne {n : ℕ} {i j : Fin n} (hji : j ≠ i) (x : SourceCubeSpace n) : (coordinateLineBase i x).ofLp j = x.ofLp j

@[simp]

theorem AleksandrovDifferentiability.coordinateLinePoint_apply_self {n : ℕ} (i : Fin n) (y : SourceCubeSpace n) (s : ℝ) : (coordinateLinePoint i y s).ofLp i = y.ofLp i + s

theorem AleksandrovDifferentiability.coordinateLinePoint_apply_ne {n : ℕ} {i j : Fin n} (hji : j ≠ i) (y : SourceCubeSpace n) (s : ℝ) : (coordinateLinePoint i y s).ofLp j = y.ofLp j

@[simp]

theorem AleksandrovDifferentiability.mem_sourceTransverseOpenCube {n : ℕ} {i : Fin n} {a : SourceTransverseSpace i} {r : ℝ} : a ∈ sourceTransverseOpenCube i r ↔ ∀ (j : { j : Fin n // j ≠ i }), |a.ofLp j| < r

@[simp]

theorem AleksandrovDifferentiability.sourceTransverseEmbed_apply_self {n : ℕ} (i : Fin n) (a : SourceTransverseSpace i) : (sourceTransverseEmbed i a).ofLp i = 0

theorem AleksandrovDifferentiability.sourceTransverseEmbed_apply_ne {n : ℕ} {i j : Fin n} (hji : j ≠ i) (a : SourceTransverseSpace i) : (sourceTransverseEmbed i a).ofLp j = a.ofLp ⟨j, hji⟩

@[simp]

theorem AleksandrovDifferentiability.sourceCoordinateChartPoint_apply_self {n : ℕ} (i : Fin n) (a : SourceTransverseSpace i) (s : ℝ) : (sourceCoordinateChartPoint i a s).ofLp i = s

theorem AleksandrovDifferentiability.sourceCoordinateChartPoint_apply_ne {n : ℕ} {i j : Fin n} (hji : j ≠ i) (a : SourceTransverseSpace i) (s : ℝ) : (sourceCoordinateChartPoint i a s).ofLp j = a.ofLp ⟨j, hji⟩

noncomputable def AleksandrovDifferentiability.sourceCoordinateChartLinearMap {n : ℕ} (i : Fin n) : WithLp 2 (SourceTransverseSpace i × ℝ) →ₗ[ℝ] SourceCubeSpace n

The coordinate chart as a linear map from the L2 product model. The ordinary product chart sourceCoordinateChartMap is obtained by precomposing this map with WithLp.toLp 2.

Equations

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

def AleksandrovDifferentiability.sourceCoordinateChartInverseLinearMap {n : ℕ} (i : Fin n) : SourceCubeSpace n →ₗ[ℝ] WithLp 2 (SourceTransverseSpace i × ℝ)

The inverse linear map to sourceCoordinateChartLinearMap, recording the transverse coordinates and the distinguished coordinate.

Equations

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

theorem AleksandrovDifferentiability.sourceCoordinateChartLinearMap_comp_inverse {n : ℕ} (i : Fin n) : sourceCoordinateChartLinearMap i ∘ₗ sourceCoordinateChartInverseLinearMap i = LinearMap.id

theorem AleksandrovDifferentiability.sourceCoordinateChartInverseLinearMap_comp {n : ℕ} (i : Fin n) : sourceCoordinateChartInverseLinearMap i ∘ₗ sourceCoordinateChartLinearMap i = LinearMap.id

theorem AleksandrovDifferentiability.sourceCoordinateChartLinearMap_norm {n : ℕ} (i : Fin n) (p : WithLp 2 (SourceTransverseSpace i × ℝ)) : ‖(sourceCoordinateChartLinearMap i) p‖ = ‖p‖

noncomputable def AleksandrovDifferentiability.sourceCoordinateChartLinearIsometryEquiv {n : ℕ} (i : Fin n) : WithLp 2 (SourceTransverseSpace i × ℝ) ≃ₗᵢ[ℝ] SourceCubeSpace n

The coordinate chart is a linear isometry equivalence from the L2 product model to the source cube.

Equations

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

@[simp]

theorem AleksandrovDifferentiability.coordinateLineBase_sourceTransverseEmbed {n : ℕ} (i : Fin n) (a : SourceTransverseSpace i) : coordinateLineBase i (sourceTransverseEmbed i a) = sourceTransverseEmbed i a

@[simp]

theorem AleksandrovDifferentiability.coordinateLineBase_sourceCoordinateChartPoint {n : ℕ} (i : Fin n) (a : SourceTransverseSpace i) (s : ℝ) : coordinateLineBase i (sourceCoordinateChartPoint i a s) = sourceTransverseEmbed i a

@[simp]

theorem AleksandrovDifferentiability.sourceCoordinateChartPoint_base_self {n : ℕ} (i : Fin n) (a : SourceTransverseSpace i) (s : ℝ) : coordinateLinePoint i (sourceTransverseEmbed i a) s = sourceCoordinateChartPoint i a s

theorem AleksandrovDifferentiability.sourceTransverseEmbed_mem_sourceOpenCube {n : ℕ} {i : Fin n} {a : SourceTransverseSpace i} {r : ℝ} (hr : 0 < r) (ha : a ∈ sourceTransverseOpenCube i r) : sourceTransverseEmbed i a ∈ sourceOpenCube n r

theorem AleksandrovDifferentiability.sourceCoordinateChartPoint_mem_sourceOpenCube {n : ℕ} {i : Fin n} {a : SourceTransverseSpace i} {s r : ℝ} (ha : a ∈ sourceTransverseOpenCube i r) (hs : |s| < r) : sourceCoordinateChartPoint i a s ∈ sourceOpenCube n r

theorem AleksandrovDifferentiability.sourceCoordinateChartPoint_mem_sourceOpenCube_iff {n : ℕ} {i : Fin n} {a : SourceTransverseSpace i} {s r : ℝ} : sourceCoordinateChartPoint i a s ∈ sourceOpenCube n r ↔ a ∈ sourceTransverseOpenCube i r ∧ |s| < r

@[simp]

theorem AleksandrovDifferentiability.coordinateLinePoint_base_self {n : ℕ} (i : Fin n) (x : SourceCubeSpace n) : coordinateLinePoint i (coordinateLineBase i x) (x.ofLp i) = x

@[simp]

theorem AleksandrovDifferentiability.coordinateLinePoint_base_add {n : ℕ} (i : Fin n) (x : SourceCubeSpace n) (h : ℝ) : coordinateLinePoint i (coordinateLineBase i x) (x.ofLp i + h) = x + h • sourceCoordinateVector i

@[simp]

theorem AleksandrovDifferentiability.coordinateLinePoint_base_sub {n : ℕ} (i : Fin n) (x : SourceCubeSpace n) (h : ℝ) : coordinateLinePoint i (coordinateLineBase i x) (x.ofLp i - h) = x - h • sourceCoordinateVector i

theorem AleksandrovDifferentiability.coordinateLineBase_mem_sourceOpenCube {n : ℕ} {i : Fin n} {x : SourceCubeSpace n} {r : ℝ} (hr : 0 < r) (hx : x ∈ sourceOpenCube n r) : coordinateLineBase i x ∈ sourceOpenCube n r

theorem AleksandrovDifferentiability.coordinateLineBase_mem_sourceOpenCube_one {n : ℕ} {i : Fin n} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) : coordinateLineBase i x ∈ sourceOpenCube n 1

@[simp]

theorem AleksandrovDifferentiability.coordinateLineBase_idem {n : ℕ} (i : Fin n) (x : SourceCubeSpace n) : coordinateLineBase i (coordinateLineBase i x) = coordinateLineBase i x

theorem AleksandrovDifferentiability.abs_sourceCoordinate_le_norm {n : ℕ} (z : SourceCubeSpace n) (i : Fin n) : |z.ofLp i| ≤ ‖z‖

Each source-coordinate of a vector is bounded by its Euclidean norm.

theorem AleksandrovDifferentiability.sourceOpenCube_one_add_norm_le_one_mem_three {n : ℕ} {x z : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) (hz : ‖z‖ ≤ 1) : x + z ∈ sourceOpenCube n 3

A displacement of Euclidean norm at most 1 from Q_1 stays inside Q_3.

theorem AleksandrovDifferentiability.sourceOpenCube_one_add_norm_le_half_mem_three_halves {n : ℕ} {x z : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) (hz : ‖z‖ ≤ 1 / 2) : x + z ∈ sourceOpenCube n (3 / 2)

A displacement of Euclidean norm at most 1 / 2 from Q_1 stays inside Q_{3/2}.

theorem AleksandrovDifferentiability.sourceOpenCube_one_add_smul_norm_le_half_mem_three_halves {n : ℕ} {x z : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) (hz : ‖z‖ ≤ 1 / 2) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : x + t • z ∈ sourceOpenCube n (3 / 2)

Small line segments from Q_1 stay inside Q_{3/2}.

theorem AleksandrovDifferentiability.eventually_sourceOpenCube_one_add_smul_mem_three_halves {n : ℕ} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) : ∀ᶠ (z : SourceCubeSpace n) in nhds 0, ∀ t ∈ Set.Icc 0 1, x + t • z ∈ sourceOpenCube n (3 / 2)

Eventually, every short segment based at a point of Q_1 lies inside Q_{3/2}.

theorem AleksandrovDifferentiability.sourceOpenCube_one_add_norm_le_two_mem_three {n : ℕ} {x z : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) (hz : ‖z‖ ≤ 2) : x + z ∈ sourceOpenCube n 3

A displacement of Euclidean norm at most 2 from Q_1 stays inside Q_3.

theorem AleksandrovDifferentiability.sourceOpenCube_three_halves_add_norm_le_three_halves_mem_three {n : ℕ} {x z : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n (3 / 2)) (hz : ‖z‖ ≤ 3 / 2) : x + z ∈ sourceOpenCube n 3

A displacement of Euclidean norm at most 3 / 2 from Q_{3/2} stays inside Q_3.

theorem AleksandrovDifferentiability.sourceOpenCube_one_sub_norm_le_one_mem_three {n : ℕ} {x z : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) (hz : ‖z‖ ≤ 1) : x - z ∈ sourceOpenCube n 3

A displacement of Euclidean norm at most 1 from Q_1 stays inside Q_3.

theorem AleksandrovDifferentiability.sourceOpenCube_one_add_coordinate_mem_three {n : ℕ} {i : Fin n} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) {h : ℝ} (hh : |h| < 2) : x + h • sourceCoordinateVector i ∈ sourceOpenCube n 3

A one-coordinate displacement of size less than 2 from Q_1 stays inside Q_3. This is the source-proof domain check for the endpoints x + h e_i.

theorem AleksandrovDifferentiability.sourceOpenCube_one_sub_coordinate_mem_three {n : ℕ} {i : Fin n} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) {h : ℝ} (hh : |h| < 2) : x - h • sourceCoordinateVector i ∈ sourceOpenCube n 3

A one-coordinate displacement of size less than 2 from Q_1 stays inside Q_3. This is the source-proof domain check for the endpoints x - h e_i.