theorem helperForTheorem_6_1_candidateFDeriv_apply {n m : ℕ} (g : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) (x₀ v : EuclideanSpace ℝ (Fin n)) : have f'fun := ∑ j : Fin n, (ContinuousLinearMap.proj j).smulRight ((EuclideanSpace.equiv (Fin m) ℝ) (g j x₀)); have f' := (↑(EuclideanSpace.equiv (Fin m) ℝ).symm).comp (f'fun.comp ↑(EuclideanSpace.equiv (Fin n) ℝ)); f' v = ∑ j : Fin n, v.ofLp j • g j x₀

Helper for Theorem 6.1: the coordinate-sum linear-map candidate evaluates to the expected finite sum ∑ j, v j • g j x₀.

theorem helperForTheorem_6_1_ball_subset_F_and_E {n : ℕ} {E F : Set (EuclideanSpace ℝ (Fin n))} {x₀ : EuclideanSpace ℝ (Fin n)} (hFE : F ⊆ E) (hx₀ : x₀ ∈ interior F) : ∃ r > 0, Metric.ball x₀ r ⊆ F ∧ Metric.ball x₀ r ⊆ E

Helper for Theorem 6.1: from interiority of x₀ in F and F ⊆ E, there is a positive radius ball around x₀ contained in both F and E.

theorem helperForTheorem_6_1_partial_closeness_single {n m : ℕ} {F : Set (EuclideanSpace ℝ (Fin n))} {x₀ : EuclideanSpace ℝ (Fin n)} (g : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) (hcont : ∀ (j : Fin n), ContinuousWithinAt (g j) F x₀) {j : Fin n} {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ x ∈ F, dist x x₀ < δ → ‖g j x - g j x₀‖ < ε

Helper for Theorem 6.1: continuity of a fixed partial-derivative field within F gives an ε-δ estimate at x₀ for that coordinate field.

theorem helperForTheorem_6_1_partial_to_lineDerivWithinAt_zero {n m : ℕ} {E F : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} (g : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) (hpartial : ∀ (j : Fin n), ∀ x ∈ F, HasPartialDerivWithinAt E f x j (g j x)) {j : Fin n} {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ F) : HasDerivWithinAt (fun (t : ℝ) => f (x + t • standardBasisVectorEuclidean n j)) (g j x) {t : ℝ | x + t • standardBasisVectorEuclidean n j ∈ E} 0

Helper for Theorem 6.1: each within-E partial derivative hypothesis at a point x ∈ F upgrades to a one-variable derivative statement along the coordinate line through x in direction e_j, at parameter value 0.

theorem helperForTheorem_6_1_uniform_partial_closeness_on_ball {n m : ℕ} {E F : Set (EuclideanSpace ℝ (Fin n))} {x₀ : EuclideanSpace ℝ (Fin n)} (hFE : F ⊆ E) (hx₀ : x₀ ∈ interior F) (g : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) (hcont : ∀ (j : Fin n), ContinuousWithinAt (g j) F x₀) {ε : ℝ} (hε : 0 < ε) : ∃ r > 0, Metric.ball x₀ r ⊆ F ∧ Metric.ball x₀ r ⊆ E ∧ ∀ (j : Fin n), ∀ x ∈ Metric.ball x₀ r, ‖g j x - g j x₀‖ ≤ ε

Helper for Theorem 6.1: continuity of all coordinate partial-derivative fields at x₀ within F gives a single radius on which all coordinates are simultaneously ε-close, and the same ball lies in both F and E.

theorem helperForTheorem_6_1_sum_standardBasisVectorEuclidean_eq {n : ℕ} (h : EuclideanSpace ℝ (Fin n)) : ∑ j : Fin n, h.ofLp j • standardBasisVectorEuclidean n j = h

Helper for Theorem 6.1: every vector in ℝⁿ is the sum of its coordinate components along the standard basis vectors.

theorem helperForTheorem_6_1_sum_range_succ_sub_eq {α : Type u_1} [AddCommGroup α] (u : ℕ → α) (n : ℕ) : ∑ i ∈ Finset.range n, (u (i + 1) - u i) = u n - u 0

Helper for Theorem 6.1: finite telescoping over successive differences on ℕ indices.

theorem helperForTheorem_6_1_sum_norm_coordinates_le_constant_mul_norm {n : ℕ} : ∃ C > 0, ∀ (h : EuclideanSpace ℝ (Fin n)), ∑ j : Fin n, ‖h.ofLp j‖ ≤ C * ‖h‖

Helper for Theorem 6.1: there is a global constant controlling the sum of coordinate norms by the ambient Euclidean norm.

theorem helperForTheorem_6_1_eta_coordinate_sum_le_eps_norm {n : ℕ} {C ε : ℝ} (hCpos : 0 < C) (hεpos : 0 < ε) (hcoordBound : ∀ (h : EuclideanSpace ℝ (Fin n)), ∑ j : Fin n, ‖h.ofLp j‖ ≤ C * ‖h‖) (h : EuclideanSpace ℝ (Fin n)) : have η := ε / (2 * C); η * ∑ j : Fin n, ‖h.ofLp j‖ ≤ ε * ‖h‖

Helper for Theorem 6.1: if η = ε / (2 * C) and coordinate norms satisfy ∑ j, ‖h j‖ ≤ C * ‖h‖, then η * (∑ j, ‖h j‖) ≤ ε * ‖h‖.

noncomputable def helperForTheorem_6_1_coordinatePrefix_nat {n : ℕ} (x₀ h : EuclideanSpace ℝ (Fin n)) (k : ℕ) : EuclideanSpace ℝ (Fin n)

Helper for Theorem 6.1: Nat-indexed coordinate-prefix path based at x₀ with increment vector h.

Equations

• helperForTheorem_6_1_coordinatePrefix_nat x₀ h k = x₀ + ∑ j : Fin n, (if ↑j < k then h.ofLp j else 0) • standardBasisVectorEuclidean n j

theorem helperForTheorem_6_1_coordinatePrefix_nat_zero {n : ℕ} (x₀ h : EuclideanSpace ℝ (Fin n)) : helperForTheorem_6_1_coordinatePrefix_nat x₀ h 0 = x₀

Helper for Theorem 6.1: the Nat-indexed coordinate-prefix path starts at x₀.

theorem helperForTheorem_6_1_coordinatePrefix_nat_succ {n : ℕ} (x₀ h : EuclideanSpace ℝ (Fin n)) {k : ℕ} (hk : k < n) : helperForTheorem_6_1_coordinatePrefix_nat x₀ h (k + 1) = helperForTheorem_6_1_coordinatePrefix_nat x₀ h k + h.ofLp ⟨k, hk⟩ • standardBasisVectorEuclidean n ⟨k, hk⟩

Helper for Theorem 6.1: one successor step in the Nat-indexed coordinate-prefix path adds the next coordinate increment.

theorem helperForTheorem_6_1_coordinatePrefix_nat_at_top {n : ℕ} (x₀ h : EuclideanSpace ℝ (Fin n)) : helperForTheorem_6_1_coordinatePrefix_nat x₀ h n = x₀ + h

Helper for Theorem 6.1: the final Nat-indexed coordinate-prefix node is x₀ + h.

theorem helperForTheorem_6_1_coordinate_segment_error_package {n m : ℕ} {E F : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ p : EuclideanSpace ℝ (Fin n)} (g : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) {j : Fin n} {hj η r : ℝ} (hpartialLine : ∀ x ∈ F, HasDerivWithinAt (fun (t : ℝ) => f (x + t • standardBasisVectorEuclidean n j)) (g j x) {t : ℝ | x + t • standardBasisVectorEuclidean n j ∈ E} 0) (hballF : Metric.ball x₀ r ⊆ F) (hclose : ∀ x ∈ Metric.ball x₀ r, ‖g j x - g j x₀‖ ≤ η) (hsegE : ∀ t ∈ segment ℝ 0 hj, p + t • standardBasisVectorEuclidean n j ∈ E) (hsegBall : ∀ t ∈ segment ℝ 0 hj, p + t • standardBasisVectorEuclidean n j ∈ Metric.ball x₀ r) : ‖f (p + hj • standardBasisVectorEuclidean n j) - f p - hj • g j x₀‖ ≤ η * ‖hj‖

Helper for Theorem 6.1: one coordinate-segment increment has remainder controlled by the uniform bound on the corresponding partial field along that segment.

theorem helperForTheorem_6_1_hasFDerivWithinAt_of_linear_remainder_bound {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)) (hbound : ∀ ε > 0, ∃ δ > 0, ∀ x ∈ E, dist x x₀ < δ → ‖f x - f x₀ - f' (x - x₀)‖ ≤ ε * ‖x - x₀‖) : HasFDerivWithinAt f f' E x₀

Helper for Theorem 6.1: a local linear remainder bound implies HasFDerivWithinAt.

theorem hasFDerivAt_of_continuous_partialDerivWithinAt {n m : ℕ} {E F : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (hFE : F ⊆ E) (hx₀ : x₀ ∈ interior F) (g : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) (hpartial : ∀ (j : Fin n), ∀ x ∈ F, HasPartialDerivWithinAt E f x j (g j x)) (hcont : ∀ (j : Fin n), ContinuousWithinAt (g j) F x₀) : ∃ (f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)), HasFDerivWithinAt f f' E x₀ ∧ ∀ (v : EuclideanSpace ℝ (Fin n)), f' v = ∑ j : Fin n, v.ofLp j • g j x₀

Theorem 6.1: Let E ⊆ ℝⁿ, let f : ℝⁿ → ℝᵐ be an ambient extension of a map on E, let F ⊆ E, and let x₀ be an interior point of F (equivalently, there is r > 0 with Metric.ball x₀ r ⊆ F). Assume that for each j ∈ {1, …, n} there is a partial-derivative field g j on F such that HasPartialDerivWithinAt E f x j (g j x) for every x ∈ F, and g j is continuous at x₀ when restricted to F. Then f is differentiable at x₀ within E, and its derivative is the linear map v ↦ ∑ j, v j • g j x₀.