noncomputable def oneSidedDirectionalDifferenceQuotientWithin {n m : ℕ} (E : Set (EuclideanSpace ℝ (Fin n))) (f : ↑E → EuclideanSpace ℝ (Fin m)) (x₀ : ↑E) (v : EuclideanSpace ℝ (Fin n)) : ℝ → EuclideanSpace ℝ (Fin m)

The one-sided directional difference quotient of f on E at x₀ in direction v.

Equations

• oneSidedDirectionalDifferenceQuotientWithin E f x₀ v t = if ht : ↑x₀ + t • v ∈ E then t⁻¹ • (f ⟨↑x₀ + t • v, ht⟩ - f x₀) else 0

def oneSidedDirectionallyDifferentiableWithinAt {n m : ℕ} (E : Set (EuclideanSpace ℝ (Fin n))) (f : ↑E → EuclideanSpace ℝ (Fin m)) (x₀ : ↑E) (v : EuclideanSpace ℝ (Fin n)) : Prop

Definition 6.9: f is one-sided directionally differentiable at the interior point x₀ in the direction v if the limit of the difference quotient along t → 0 with t > 0 and x₀ + t v ∈ E exists.

Equations

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

noncomputable def oneSidedDirectionalDerivWithin {n m : ℕ} (E : Set (EuclideanSpace ℝ (Fin n))) (f : ↑E → EuclideanSpace ℝ (Fin m)) (x₀ : ↑E) (v : EuclideanSpace ℝ (Fin n)) (h : oneSidedDirectionallyDifferentiableWithinAt E f x₀ v) : EuclideanSpace ℝ (Fin m)

The one-sided directional derivative Dᵥ f(x₀) as the limit value, assuming the directional derivative exists in the sense of one-sided directional differentiability.

Equations

• oneSidedDirectionalDerivWithin E f x₀ v h = Classical.choose ⋯

theorem helperForLemma_6_6_zero_mem_directionConstraint {n : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {x₀ v : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) : 0 ∈ {t : ℝ | x₀ + t • v ∈ E}

Helper for Lemma 6.6: if x₀ is an interior point of E, then t = 0 belongs to the directional-constraint set {t | x₀ + t • v ∈ E}.

theorem helperForLemma_6_6_tendsto_nhdsWithin_zero_forces_value {m : ℕ} {s : Set ℝ} {g : ℝ → EuclideanSpace ℝ (Fin m)} {L : EuclideanSpace ℝ (Fin m)} (hs : 0 ∈ s) (hlim : Filter.Tendsto g (nhdsWithin 0 s) (nhds L)) : g 0 = L

Helper for Lemma 6.6: a nhdsWithin limit at 0 over a set containing 0 fixes the function value at 0.

theorem helperForLemma_6_6_differenceQuotient_valueAtZero {n m : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} : (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) 0 = 0

Helper for Lemma 6.6: the directional difference quotient in the theorem statement has value 0 at t = 0.

theorem helperForLemma_6_6_unpunctured_limit_forces_zero {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hlim : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))) : f' v = 0

Helper for Lemma 6.6: any limit claim in the theorem's unpunctured nhdsWithin filter forces the claimed limit value to be 0.

theorem helperForLemma_6_6_no_unpunctured_limit_of_ne_zero {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hv : f' v ≠ 0) : ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: if f' v ≠ 0, then the theorem's unpunctured directional-limit statement cannot hold.

theorem helperForLemma_6_6_id_hasFDerivWithinAt_univ {n : ℕ} (x₀ : EuclideanSpace ℝ (Fin n)) : HasFDerivWithinAt (fun (x : EuclideanSpace ℝ (Fin n)) => x) (ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin n))) Set.univ x₀

Helper for Lemma 6.6: the identity map has derivative id within univ at every point.

theorem helperForLemma_6_6_identity_differenceQuotient_of_ne_zero {n : ℕ} {x₀ v : EuclideanSpace ℝ (Fin n)} {t : ℝ} (ht : t ≠ 0) : t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin n)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin n)) => x) x₀) = v

Helper for Lemma 6.6: for nonzero t, the identity-map directional quotient simplifies to the direction vector v.

theorem helperForLemma_6_6_identity_punctured_directional_limit {n : ℕ} {x₀ v : EuclideanSpace ℝ (Fin n)} : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin n)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin n)) => x) x₀)) (nhdsWithin 0 {0}ᶜ) (nhds v)

Helper for Lemma 6.6: the identity map has the expected punctured directional limit t → 0, t ≠ 0, namely v.

theorem helperForLemma_6_6_unpunctured_identity_limit_impossible {n : ℕ} {x₀ v : EuclideanSpace ℝ (Fin n)} (hv : v ≠ 0) : ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin n)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin n)) => x) x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ Set.univ}) (nhds ((ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin n))) v))

Helper for Lemma 6.6: for nonzero direction v, the theorem's unpunctured directional-limit conclusion fails for the identity map on ℝⁿ.

theorem helperForLemma_6_6_identity_counterexample_data {n : ℕ} {x₀ v : EuclideanSpace ℝ (Fin n)} (hv : v ≠ 0) : ∃ (_ : HasFDerivWithinAt (fun (x : EuclideanSpace ℝ (Fin n)) => x) (ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin n))) Set.univ x₀), ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin n)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin n)) => x) x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ Set.univ}) (nhds ((ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin n))) v))

Helper for Lemma 6.6: for any nonzero direction, the identity map on univ provides concrete derivative data together with failure of the unpunctured directional-limit conclusion.

theorem helperForLemma_6_6_standardBasisVector_finOne_ne_zero : EuclideanSpace.single ⟨0, ⋯⟩ 1 ≠ 0

Helper for Lemma 6.6: in dimension 1, the standard basis direction e₀ is nonzero.

theorem helperForLemma_6_6_unpunctured_identity_counterexample_finOne : ∃ (x₀ : EuclideanSpace ℝ (Fin 1)) (v : EuclideanSpace ℝ (Fin 1)), ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin 1)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin 1)) => x) x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ Set.univ}) (nhds ((ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin 1))) v))

Helper for Lemma 6.6: there is a concrete dimension-1 counterexample witness to the unpunctured directional-limit claim (identity map on univ and direction e₀).

theorem helperForLemma_6_6_finOne_identity_punctured_limit_and_unpunctured_failure : ∃ (x₀ : EuclideanSpace ℝ (Fin 1)) (v : EuclideanSpace ℝ (Fin 1)), Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin 1)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin 1)) => x) x₀)) (nhdsWithin 0 {0}ᶜ) (nhds v) ∧ ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin 1)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin 1)) => x) x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ Set.univ}) (nhds v)

Helper for Lemma 6.6: in dimension 1, the identity map at the concrete direction e₀ has the expected punctured directional limit, while the unpunctured target-limit claim still fails.

theorem helperForLemma_6_6_identity_unpunctured_limit_forces_direction_zero {n : ℕ} {x₀ v : EuclideanSpace ℝ (Fin n)} (hlim : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • ((fun (x : EuclideanSpace ℝ (Fin n)) => x) (x₀ + t • v) - (fun (x : EuclideanSpace ℝ (Fin n)) => x) x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ Set.univ}) (nhds ((ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin n))) v))) : v = 0

Helper for Lemma 6.6: for the identity map on univ, any unpunctured directional limit at 0 forces the direction vector to be 0.

theorem helperForLemma_6_6_hasFDerivAt_of_hasFDerivWithinAt_interior {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)} (hx₀ : x₀ ∈ interior E) (hfd : HasFDerivWithinAt f f' E x₀) : HasFDerivAt f f' x₀

Helper for Lemma 6.6: interior-point differentiability within E upgrades to ambient Fréchet differentiability at the same base point.

theorem helperForLemma_6_6_tendsto_directionalQuotient_on_punctured_nhds {n m : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hfdAt : HasFDerivAt f f' x₀) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {0}ᶜ) (nhds (f' v))

Helper for Lemma 6.6: an ambient Fréchet derivative yields the punctured directional difference-quotient limit along 𝓝[≠] 0.

theorem helperForLemma_6_6_mono_to_constrainted_punctured_filter {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hpunctured : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {0}ᶜ) (nhds (f' v))) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | t ≠ 0 ∧ x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: a punctured-neighborhood directional limit remains valid after restricting the source filter to points with x₀ + t • v ∈ E.

theorem helperForLemma_6_6_punctured_directional_limit_of_hasFDerivWithinAt {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hfd : HasFDerivWithinAt f f' E x₀) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | t ≠ 0 ∧ x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: the punctured directional-quotient formulation is derivable from a within-domain Fréchet derivative at an interior point.

theorem helperForLemma_6_6_hasDirectionalDerivWithinAt_eq_fderiv_punctured {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hfd : HasFDerivWithinAt f f' E x₀) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | t ≠ 0 ∧ x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: differentiability at an interior point yields the punctured directional-difference-quotient limit to f' v, i.e. the mathematically correct directional limit statement with t ≠ 0 explicitly enforced in the source filter.

theorem helperForLemma_6_6_hasDirectionalDerivWithinAt_eq_fderiv_corrected {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hfd : HasFDerivWithinAt f f' E x₀) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | t ≠ 0 ∧ x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: corrected directional-derivative statement using the punctured source filter (t ≠ 0), matching the mathematically valid formulation.

theorem helperForLemma_6_6_target_claim_forces_zero {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hclaim : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))) : f' v = 0

Helper for Lemma 6.6: if the theorem's unpunctured directional-limit claim holds for given data, then the directional value f' v is forced to be zero.

theorem helperForLemma_6_6_nonzero_directionalValue_precludes_unpunctured_target {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hv0 : f' v ≠ 0) : ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: at an interior point, any unpunctured directional-limit claim with nonzero directional value is contradictory; this obstruction does not use differentiability.

theorem helperForLemma_6_6_directionConstraint_eq_insert_zero_punctured {n : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {x₀ v : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) : {t : ℝ | x₀ + t • v ∈ E} = insert 0 {t : ℝ | t ≠ 0 ∧ x₀ + t • v ∈ E}

Helper for Lemma 6.6: at an interior point, the unpunctured directional-constraint set is obtained by inserting 0 into the punctured constraint set.

theorem helperForLemma_6_6_unpunctured_limit_of_punctured_limit_and_zero_directional_value {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hpunctured : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | t ≠ 0 ∧ x₀ + t • v ∈ E}) (nhds (f' v))) (hv0 : f' v = 0) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: if the punctured directional quotient tends to f' v and that value is 0, then the corresponding unpunctured directional limit follows.

theorem helperForLemma_6_6_unpunctured_limit_iff_zero_of_punctured_limit {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hx₀ : x₀ ∈ interior E) (hpunctured : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | t ≠ 0 ∧ x₀ + t • v ∈ E}) (nhds (f' v))) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v)) ↔ f' v = 0

Helper for Lemma 6.6: once the punctured directional quotient converges to f' v, the unpunctured directional-limit claim is equivalent to the vanishing condition f' v = 0.

theorem helperForLemma_6_6_explicit_unpunctured_counterexample_data : ∃ (E : Set (EuclideanSpace ℝ (Fin 1))) (f : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)) (x₀ : EuclideanSpace ℝ (Fin 1)) (v : EuclideanSpace ℝ (Fin 1)) (f' : EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1)), x₀ ∈ interior E ∧ HasFDerivWithinAt f f' E x₀ ∧ ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: there exists explicit differentiable data (identity map on univ in dimension 1) for which the theorem's unpunctured directional-limit conclusion fails.

theorem helperForLemma_6_6_explicit_unpunctured_counterexample_data_with_nonzero_value : ∃ (E : Set (EuclideanSpace ℝ (Fin 1))) (f : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)) (x₀ : EuclideanSpace ℝ (Fin 1)) (v : EuclideanSpace ℝ (Fin 1)) (f' : EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1)), x₀ ∈ interior E ∧ HasFDerivWithinAt f f' E x₀ ∧ f' v ≠ 0 ∧ ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: there is explicit differentiable data (identity map on univ in dimension 1) where the unpunctured directional-limit conclusion fails and the claimed limit value f' v is nonzero.

theorem helperForLemma_6_6_unpunctured_universal_claim_false : ¬∀ {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)}, x₀ ∈ interior E → ∀ {v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)}, HasFDerivWithinAt f f' E x₀ → Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: the unpunctured directional-limit conclusion cannot hold as a universal theorem; the explicit dimension-1 identity-map data is a counterexample.

theorem helperForLemma_6_6_unpunctured_nonzero_directional_universal_claim_false : ¬∀ {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)}, x₀ ∈ interior E → ∀ {v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)}, HasFDerivWithinAt f f' E x₀ → f' v ≠ 0 → Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: even after restricting to nonzero directional values f' v ≠ 0, the unpunctured directional-limit conclusion is still not universally valid.

theorem helperForLemma_6_6_target_tendsto_iff_directionalValue_eq_zero {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) {v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hfd : HasFDerivWithinAt f f' E x₀) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v)) ↔ f' v = 0

Helper for Lemma 6.6: for fixed differentiable data, the theorem's unpunctured directional-limit claim is equivalent to the directional value f' v being zero.

theorem helperForLemma_6_6_not_target_tendsto_of_nonzero_directionalValue {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) {v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hfd : HasFDerivWithinAt f f' E x₀) (hv0 : f' v ≠ 0) : ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: if the directional value f' v is nonzero, then the theorem's unpunctured directional-limit claim is impossible for that fixed differentiable data.

theorem helperForLemma_6_6_not_target_tendsto_iff_nonzero_directionalValue {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) {v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hfd : HasFDerivWithinAt f f' E x₀) : ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v)) ↔ f' v ≠ 0

Helper for Lemma 6.6: for fixed differentiable data at an interior point, failure of the unpunctured directional-limit target is equivalent to the directional value being nonzero.

theorem helperForLemma_6_6_all_unpunctured_targets_force_zero_fderiv {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hall : ∀ (w : EuclideanSpace ℝ (Fin n)), Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • w) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • w ∈ E}) (nhds (f' w))) : f' = 0

Helper for Lemma 6.6: if the theorem's unpunctured directional-limit conclusion held for every direction (for fixed data at an interior point), then the derivative map would be the zero linear map.

theorem helperForLemma_6_6_target_proof_contradicts_nonzero_directionalValue {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) {v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hfd : HasFDerivWithinAt f f' E x₀) (hv0 : f' v ≠ 0) (htarget : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))) : False

Helper for Lemma 6.6: for fixed differentiable data, any proof of the theorem's unpunctured directional-limit target contradicts a nonzero directional value f' v.

theorem helperForLemma_6_6_not_target_of_targetIff_directionalValue_eq_zero {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (htargetIffZero : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v)) ↔ f' v = 0) (hv0 : f' v ≠ 0) : ¬Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v))

Helper for Lemma 6.6: if the theorem's target claim is equivalent to the vanishing directional value f' v = 0, then any nonzero directional value excludes that target claim.

theorem helperForLemma_6_6_targetIffFalse_of_targetIffZero_and_nonzero_directionalValue {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (htargetIffZero : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v)) ↔ f' v = 0) (hv0 : f' v ≠ 0) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v)) ↔ False

Helper for Lemma 6.6: if the theorem's target claim is equivalent to f' v = 0, then under f' v ≠ 0 that target claim is equivalent to False.

theorem helperForLemma_6_6_targetIffFalse_of_nonzero_directionalValue {n m : ℕ} {E : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {x₀ : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ interior E) {v : EuclideanSpace ℝ (Fin n)} {f' : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)} (hfd : HasFDerivWithinAt f f' E x₀) (hv0 : f' v ≠ 0) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x₀ + t • v) - f x₀)) (nhdsWithin 0 {t : ℝ | x₀ + t • v ∈ E}) (nhds (f' v)) ↔ False

Helper for Lemma 6.6: for fixed differentiable data at an interior point, if f' v ≠ 0, then the theorem's unpunctured target statement is equivalent to False.