Helper for Lemma 6.6: when the directional value f' v is zero, the theorem's
unpunctured directional-limit target follows from the established equivalence with
f' v = 0.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, if
f' v ≠ 0 then any proof of the theorem's unpunctured directional-limit target yields
False.
Helper for Lemma 6.6: any implication that turns differentiability data into the theorem's
unpunctured directional-limit target forces the directional value f' v to be zero.
Helper for Lemma 6.6: with fixed differentiability data, a nonzero directional value makes any implication to the theorem's unpunctured target claim contradictory.
Helper for Lemma 6.6: once differentiability data is fixed, a nonzero directional value precludes any implication from that data to the theorem's unpunctured target claim.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, if
f' v ≠ 0 then the theorem's unpunctured directional-limit target is equivalent to
False.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, the theorem's
unpunctured directional-limit target is equivalent to the conjunction of the punctured
directional limit and the vanishing directional value f' v = 0.
Helper for Lemma 6.6: if the theorem's unpunctured target claim is equivalent to
f' v = 0 together with the punctured directional-limit claim, then any nonzero
directional value f' v excludes the unpunctured target claim.
Helper for Lemma 6.6: for fixed differentiability data at an interior point,
combining a nonzero directional value f' v ≠ 0 with the theorem's unpunctured
target claim yields a contradiction.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, if
f' v ≠ 0 then the theorem's unpunctured directional-limit target proposition is empty.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, if
f' v ≠ 0 then the theorem's unpunctured directional-limit target proposition has no
inhabitants.
Helper for Lemma 6.6: if the theorem's unpunctured directional-limit target proposition is
inhabited for fixed interior-point data, then the directional value f' v must be zero.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, inhabitation of
the theorem's unpunctured directional-limit target proposition is equivalent to f' v = 0.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, the theorem's
unpunctured directional-limit target proposition is empty exactly when the directional value
f' v is nonzero.
Helper for Lemma 6.6: for fixed differentiable data at an interior point, if
f' v ≠ 0 then inhabitation of the theorem's unpunctured directional-limit target proposition
is equivalent to False.
Helper for Lemma 6.6: in the nonzero directional-value branch, differentiability still gives the punctured directional limit, while the theorem's unpunctured target proposition is empty.
Lemma 6.6: Let E ⊆ ℝⁿ, f : E → ℝᵐ (represented by an ambient map with
within-domain derivative), and x₀ ∈ interior E. If f is differentiable at x₀
within E with derivative f', then the directional derivative at x₀ in direction v
exists as t → 0 along nonzero points with x₀ + t v ∈ E, and equals f' v.
The difference quotient used to define the partial derivative of f with respect to the
j-th coordinate at x₀.
Equations
- partialDifferenceQuotientWithin f x₀ j t = t⁻¹ • (f (x₀ + t • standardBasisVectorEuclidean n j) - f x₀)
Instances For
The within-E partial derivative notion (equation 6.u77): for E ⊆ ℝⁿ, ambient extension
f : ℝⁿ → ℝᵐ of the book map E → ℝᵐ, interior x₀ ∈ E, and coordinate j,
HasPartialDerivWithinAt E f x₀ j L records that the constrained difference quotient along e_j
converges to L as t → 0 through nonzero values with x₀ + t e_j ∈ E.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Definition 6.10: f is continuously differentiable on E if E consists of interior points
and for each coordinate direction j, there is a map gⱼ : ℝⁿ → ℝᵐ that is continuous on E
and satisfies gⱼ x = ∂f/∂xⱼ (x) for every x ∈ E in the within-E sense (using equation 6.u77);
the companion declarations below encode equations 6.u78–6.u80.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Definition 6.11: Let E ⊆ ℝⁿ, f : ℝⁿ → ℝᵐ (an ambient extension of a map on E), and
x₀ ∈ E such that for every coordinate j the partial derivative of f at x₀ within E
exists. The derivative (Jacobian) matrix Df(x₀) is the m × n matrix whose (i,j)-entry is
∂fᵢ/∂xⱼ (x₀).
Equations
- derivativeMatrixWithinAt E f x₀ hpartial i j = (Classical.choose ⋯).ofLp i
Instances For
For vector-valued maps, the partial derivative in one coordinate direction is determined by
the partial derivatives of the component functions fun x => (f x) k (equation 6.u78).
If f has Fréchet derivative f' at x₀ within E, then its j-th partial derivative at
x₀ exists and equals f' e_j.
If f has ambient Fréchet derivative f' at x₀, then at an interior point of E its
j-th partial derivative within E exists and equals f' e_j (equation 6.u79).
A linear derivative map sends a direction v = ∑ⱼ vⱼ eⱼ to
∑ⱼ vⱼ (f' eⱼ), matching the directional derivative expansion by partial derivatives.
If f has Fréchet derivative within E at x₀, and if L j are the corresponding
partial derivatives at x₀, then the directional derivative in any direction v equals
∑ⱼ vⱼ • L j (equation 6.u80).
Proposition 6.9: Let E ⊆ ℝⁿ, f : ℝⁿ → ℝᵐ, and x₀ ∈ E.
Assume f is differentiable at x₀ within E with derivative f', and let
Df be the Jacobian matrix representing f' (so f' = Matrix.mulVecLin Df).
Then for every direction v, the directional derivative exists and
(Dᵥ f(x₀))ᵀ = Df * vᵀ, i.e. the directional derivative limit is Matrix.mulVec Df v.
Equivalently, Dᵥ f(x₀) = f' v = ∑ⱼ vⱼ • (f' eⱼ).