def HasDerivativeInOneVariableAt (E : Set ℝ) (f : ↑E → ℝ) (x₀ : ↑E) (L : ℝ) : Prop

Definition 6.7 (Derivative in one variable): let E ⊆ ℝ, f : E → ℝ, and x₀ ∈ E. A real number L is the derivative of f at x₀ iff (f x - f x₀) / (x - x₀) tends to L as x → x₀ with x ∈ E \ {x₀}.

Equations

• HasDerivativeInOneVariableAt E f x₀ L = Filter.Tendsto (fun (x : ↑E) => (f x - f x₀) / (↑x - ↑x₀)) (nhdsWithin x₀ {x : ↑E | ↑x ≠ ↑x₀}) (nhds L)

theorem helperForLemma_6_4_pointwise_absErrorRatio_eq_absQuotientSub (E : Set ℝ) (f : ↑E → ℝ) (x₀ : ↑E) (L : ℝ) (x : ↑E) (hx : ↑x ≠ ↑x₀) : |f x - (f x₀ + L * (↑x - ↑x₀))| / |↑x - ↑x₀| = |(f x - f x₀) / (↑x - ↑x₀) - L|

Helper for Lemma 6.4: pointwise algebraic identity relating the linearization error ratio and the absolute difference quotient error.

theorem helperForLemma_6_4_eventually_ne_basepoint_on_puncturedFilter (E : Set ℝ) (x₀ : ↑E) : ∀ᶠ (x : ↑E) in nhdsWithin x₀ {x : ↑E | ↑x ≠ ↑x₀}, ↑x ≠ ↑x₀

Helper for Lemma 6.4: on the punctured nhdsWithin filter, points are eventually different from the basepoint.

theorem helperForLemma_6_4_eventuallyEq_errorRatio_absSubForm (E : Set ℝ) (f : ↑E → ℝ) (x₀ : ↑E) (L : ℝ) : (fun (x : ↑E) => |f x - (f x₀ + L * (↑x - ↑x₀))| / |↑x - ↑x₀|) =ᶠ[nhdsWithin x₀ {x : ↑E | ↑x ≠ ↑x₀}] fun (x : ↑E) => |(f x - f x₀) / (↑x - ↑x₀) - L|

Helper for Lemma 6.4: eventual equality between the target error ratio and the absolute form |quotient - L| on the punctured filter.

theorem hasDerivativeInOneVariableAt_iff_tendsto_normErrorRatio_zero (E : Set ℝ) (f : ↑E → ℝ) (x₀ : ↑E) (L : ℝ) (hlimit : ↑x₀ ∈ closure (E \ {↑x₀})) : HasDerivativeInOneVariableAt E f x₀ L ↔ Filter.Tendsto (fun (x : ↑E) => |f x - (f x₀ + L * (↑x - ↑x₀))| / |↑x - ↑x₀|) (nhdsWithin x₀ {x : ↑E | ↑x ≠ ↑x₀}) (nhds 0)

Lemma 6.4: let E ⊆ ℝ, f : E → ℝ, x₀ ∈ E a limit point of E, and L ∈ ℝ. Then (f x - f x₀) / (x - x₀) → L as x → x₀ in E \ {x₀} iff |f x - (f x₀ + L (x - x₀))| / |x - x₀| → 0 on the same punctured domain.

def HasDerivativeInSeveralVariablesAt (n m : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (f : ↑E → EuclideanSpace ℝ (Fin m)) (x₀ : ↑E) (L : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : Prop

Definition 6.8 (Differentiability): let E ⊆ ℝ^n, f : E → ℝ^m, and x₀ ∈ E be a limit point of E. For a linear map L : ℝ^n → ℝ^m, f is differentiable at x₀ with derivative L when ‖f x - (f x₀ + L (x - x₀))‖ / ‖x - x₀‖ → 0 as x → x₀ with x ∈ E \ {x₀}, using the Euclidean norm.

Equations

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

theorem helperForProposition_6_8_memClosure_univ_diff_singleton (x₀ : EuclideanSpace ℝ (Fin 2)) : x₀ ∈ closure (Set.univ \ {x₀})

Helper for Proposition 6.8: the basepoint lies in the closure of the punctured universe.

theorem helperForProposition_6_8_f_eq_coordinateSquare_onSubtypeUniv (f : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ } → EuclideanSpace ℝ (Fin 2)) (hf₀ : ∀ (p : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }), (f p).ofLp 0 = (↑p).ofLp 0 ^ 2) (hf₁ : ∀ (p : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }), (f p).ofLp 1 = (↑p).ofLp 1 ^ 2) (p : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }) : f p = (EuclideanSpace.equiv (Fin 2) ℝ).symm fun (i : Fin 2) => (↑p).ofLp i ^ 2

Helper for Proposition 6.8: the map f agrees with the coordinate-square formula.

theorem helperForProposition_6_8_hasFDerivAt_coordinateSquare_at_x0 (x₀ : EuclideanSpace ℝ (Fin 2)) (hx₀₀ : x₀.ofLp 0 = 1) (hx₀₁ : x₀.ofLp 1 = 2) (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) (hL₀ : ∀ (v : EuclideanSpace ℝ (Fin 2)), (L v).ofLp 0 = 2 * v.ofLp 0) (hL₁ : ∀ (v : EuclideanSpace ℝ (Fin 2)), (L v).ofLp 1 = 4 * v.ofLp 1) : HasFDerivAt (fun (x : EuclideanSpace ℝ (Fin 2)) => (EuclideanSpace.equiv (Fin 2) ℝ).symm fun (i : Fin 2) => x.ofLp i ^ 2) (LinearMap.toContinuousLinearMap L) x₀

Helper for Proposition 6.8: the coordinate-square ambient map has derivative L at x₀.

theorem helperForProposition_6_8_tendsto_errorRatio_on_puncturedAmbient (x₀ : EuclideanSpace ℝ (Fin 2)) (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) (hFDeriv : HasFDerivAt (fun (x : EuclideanSpace ℝ (Fin 2)) => (EuclideanSpace.equiv (Fin 2) ℝ).symm fun (i : Fin 2) => x.ofLp i ^ 2) (LinearMap.toContinuousLinearMap L) x₀) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin 2)) => ‖((EuclideanSpace.equiv (Fin 2) ℝ).symm fun (i : Fin 2) => x.ofLp i ^ 2) - (((EuclideanSpace.equiv (Fin 2) ℝ).symm fun (i : Fin 2) => x₀.ofLp i ^ 2) + L (x - x₀))‖ / ‖x - x₀‖) (nhdsWithin x₀ {x : EuclideanSpace ℝ (Fin 2) | x ≠ x₀}) (nhds 0)

Helper for Proposition 6.8: the linearization error ratio tends to 0 on punctured neighborhoods in the ambient space.

theorem helperForProposition_6_8_nhdsWithin_puncturedSubtypeUniv_eq_comap (x₀ : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }) : nhdsWithin x₀ {x : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ } | x ≠ x₀} = Filter.comap (fun (x : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }) => ↑x) (nhdsWithin ↑x₀ {x : EuclideanSpace ℝ (Fin 2) | x ≠ ↑x₀})

Helper for Proposition 6.8: punctured neighborhood filters on Subtype univ agree with the ambient punctured filter via coercion.

theorem hasDerivativeInSeveralVariablesAt_coordinateSquare_at_one_two (x₀ : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }) (hx₀₀ : (↑x₀).ofLp 0 = 1) (hx₀₁ : (↑x₀).ofLp 1 = 2) (f : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ } → EuclideanSpace ℝ (Fin 2)) (hf₀ : ∀ (p : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }), (f p).ofLp 0 = (↑p).ofLp 0 ^ 2) (hf₁ : ∀ (p : { x : EuclideanSpace ℝ (Fin 2) // x ∈ Set.univ }), (f p).ofLp 1 = (↑p).ofLp 1 ^ 2) (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) (hL₀ : ∀ (v : EuclideanSpace ℝ (Fin 2)), (L v).ofLp 0 = 2 * v.ofLp 0) (hL₁ : ∀ (v : EuclideanSpace ℝ (Fin 2)), (L v).ofLp 1 = 4 * v.ofLp 1) : HasDerivativeInSeveralVariablesAt 2 2 Set.univ f x₀ L

Proposition 6.8: if f : ℝ² → ℝ² is given by f(x, y) = (x^2, y^2), then f is differentiable at x₀ = (1, 2) with derivative L(x, y) = (2x, 4y).

theorem derivativeInSeveralVariables_unique (n m : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (f : ↑E → EuclideanSpace ℝ (Fin m)) (x₀ : ↑E) (hinterior : ↑x₀ ∈ interior E) (L₁ L₂ : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (hL₁ : HasDerivativeInSeveralVariablesAt n m E f x₀ L₁) (hL₂ : HasDerivativeInSeveralVariablesAt n m E f x₀ L₂) : L₁ = L₂

Lemma 6.5 (Uniqueness of derivatives): if x₀ is an interior point of E ⊆ ℝⁿ and both L₁ and L₂ satisfy the derivative error-ratio limit for f : E → ℝᵐ at x₀, then the linear transformations coincide: L₁ = L₂.