def graphOfFunction {n : ℕ} (f : (Fin n → ℝ) → ℝ) : Set (Fin (n + 1) → ℝ)

Definition 6.16 (Graph of a function): for f : ℝ^n → ℝ, the graph of f is the subset {(x, f x) : x ∈ ℝ^n} of ℝ^(n+1).

Equations

• graphOfFunction f = Set.range fun (x : Fin n → ℝ) => Fin.snoc x (f x)

theorem verticalLineTest (S : Set (ℝ × ℝ)) : (∃ (f : ℝ → ℝ), S = Set.range fun (x : ℝ) => (x, f x)) ↔ ∀ (x : ℝ), ∃! y : ℝ, (x, y) ∈ S

Definition 6.17 (Vertical line test): a subset S ⊆ ℝ² is the graph of some function f : ℝ → ℝ if and only if for every x : ℝ there exists a unique y : ℝ such that (x, y) ∈ S.

def hypersurfaceDefinedBy (n : ℕ) (g : (Fin n → ℝ) → ℝ) : Set (Fin n → ℝ)

Definition 6.18 (Hypersurface defined by an equation): for g : ℝ^n → ℝ, the hypersurface (level set) defined by g is Z(g) = {x ∈ ℝ^n | g x = 0}.

Equations

• hypersurfaceDefinedBy n g = {x : Fin n → ℝ | g x = 0}

def IsCriticalPoint {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x₀ : Fin n → ℝ) : Prop

Definition 6.19 (Critical point): for a differentiable function f : ℝ^n → ℝ, a point x₀ is a critical point of f when ∇ f(x₀) = 0. In finite-dimensional coordinates, this is expressed as differentiability at x₀ and vanishing Fréchet derivative there.

Equations

• IsCriticalPoint f x₀ = (DifferentiableAt ℝ f x₀ ∧ fderiv ℝ f x₀ = 0)

noncomputable def partialDerivWithin {n : ℕ} (f : (Fin n → ℝ) → ℝ) (s : Set (Fin n → ℝ)) (x : Fin n → ℝ) (i : Fin n) : ℝ

The coordinate-direction derivative of a scalar function on ℝ^n within a set.

Equations

• partialDerivWithin f s x i = (fderivWithin ℝ f s x) (Pi.single i 1)

theorem helperForTheorem_6_11_realLinearMap_bijective_of_map_one_ne_zero (L : ℝ →L[ℝ] ℝ) (hL : L 1 ≠ 0) : Function.Bijective ⇑L

Helper for Theorem 6.11: a continuous linear map ℝ →L[ℝ] ℝ is bijective if it is nonzero at 1.

theorem helperForTheorem_6_11_lastPartial_ne_zero_fderiv {n : ℕ} {E : Set (Fin (n + 1) → ℝ)} {f : (Fin (n + 1) → ℝ) → ℝ} {y' : Fin n → ℝ} {yLast : ℝ} (hEopen : IsOpen E) (hf : ContDiffOn ℝ 1 f E) (hy : Fin.snoc y' yLast ∈ E) (hpartial : partialDerivWithin f E (Fin.snoc y' yLast) (Fin.last n) ≠ 0) : (fderiv ℝ f (Fin.snoc y' yLast)) (Pi.single (Fin.last n) 1) ≠ 0

Helper for Theorem 6.11: convert the nonvanishing within-partial at the base point to the ambient Fréchet derivative coordinate being nonzero.

theorem helperForTheorem_6_11_uniqueness_from_graph_equality {n : ℕ} {f : (Fin (n + 1) → ℝ) → ℝ} {U : Set (Fin n → ℝ)} {V : Set (Fin (n + 1) → ℝ)} {g g2 : (Fin n → ℝ) → ℝ} (hA : {x : Fin (n + 1) → ℝ | x ∈ V ∧ f x = 0} = (fun (x' : Fin n → ℝ) => Fin.snoc x' (g x')) '' U) (hA2 : {x : Fin (n + 1) → ℝ | x ∈ V ∧ f x = 0} = (fun (x' : Fin n → ℝ) => Fin.snoc x' (g2 x')) '' U) (x' : Fin n → ℝ) : x' ∈ U → g2 x' = g x'

Helper for Theorem 6.11: graph equality determines the implicit function uniquely on U.

theorem implicitFunctionTheorem (n : ℕ) (E : Set (Fin (n + 1) → ℝ)) (f : (Fin (n + 1) → ℝ) → ℝ) (y' : Fin n → ℝ) (yLast : ℝ) (hEopen : IsOpen E) (hf : ContDiffOn ℝ 1 f E) (hy : Fin.snoc y' yLast ∈ E) (hyZero : f (Fin.snoc y' yLast) = 0) (hpartial : partialDerivWithin f E (Fin.snoc y' yLast) (Fin.last n) ≠ 0) : ∃ (U : Set (Fin n → ℝ)), IsOpen U ∧ y' ∈ U ∧ ∃ (V : Set (Fin (n + 1) → ℝ)), IsOpen V ∧ Fin.snoc y' yLast ∈ V ∧ V ⊆ E ∧ have A := fun (g : (Fin n → ℝ) → ℝ) => g y' = yLast ∧ {x : Fin (n + 1) → ℝ | x ∈ V ∧ f x = 0} = (fun (x' : Fin n → ℝ) => Fin.snoc x' (g x')) '' U; have B := fun (g : (Fin n → ℝ) → ℝ) => ContDiffOn ℝ 1 g U ∧ ∀ x' ∈ U, ∀ (j : Fin n), partialDerivWithin g U x' j = -(partialDerivWithin f E (Fin.snoc x' (g x')) j.castSucc / partialDerivWithin f E (Fin.snoc x' (g x')) (Fin.last n)); ∃ (g : (Fin n → ℝ) → ℝ), A g ∧ B g ∧ ∀ (g2 : (Fin n → ℝ) → ℝ), A g2 → ∀ x' ∈ U, g2 x' = g x'

Theorem 6.11 (Implicit function theorem): in ambient coordinates (x', x_{n+1}) ∈ ℝ^(n+1) (corresponding to the book's ℝ^n after reindexing), if E ⊆ ℝ^(n+1) is open, f is continuously differentiable on E, f (y', yLast) = 0, and ∂f/∂x_{n+1} (y', yLast) ≠ 0, then there are open sets U, V with (y', yLast) ∈ V, y' ∈ U, and a C^1 function g whose graph over U cuts out the zero set of f in V; moreover this g is unique on U and satisfies the usual derivative quotient formula in each x'-direction.

theorem helperForProposition_6_17_constraintEventuallyEqZero {m : ℕ} {V : Set (Fin m → ℝ)} {f : (Fin (m + 1) → ℝ) → ℝ} {g : (Fin m → ℝ) → ℝ} {x : Fin m → ℝ} (hconstraint : ∀ z ∈ V, f (Fin.snoc z (g z)) = 0) : (fun (z : Fin m → ℝ) => f (Fin.snoc z (g z))) =ᶠ[nhdsWithin x V] fun (x : Fin m → ℝ) => 0

Helper for Proposition 6.17: turn the pointwise constraint on V into an eventual equality with the constant zero function within V.

noncomputable def helperForProposition_6_17_DGx {m : ℕ} (g : (Fin m → ℝ) → ℝ) (V : Set (Fin m → ℝ)) (x : Fin m → ℝ) : (Fin m → ℝ) →L[ℝ] Fin (m + 1) → ℝ

Helper for Proposition 6.17: the derivative of the map z ↦ (z, g z) within V.

Equations

• helperForProposition_6_17_DGx g V x = ContinuousLinearMap.pi fun (i : Fin (m + 1)) => Fin.lastCases (fderivWithin ℝ g V x) (fun (k : Fin m) => ContinuousLinearMap.proj k) i

theorem helperForProposition_6_17_compositionHasFDerivWithinAt {m : ℕ} {U : Set (Fin (m + 1) → ℝ)} {V : Set (Fin m → ℝ)} {f : (Fin (m + 1) → ℝ) → ℝ} {g : (Fin m → ℝ) → ℝ} {x : Fin m → ℝ} (hx : x ∈ V) (hf : DifferentiableOn ℝ f U) (hg : DifferentiableOn ℝ g V) (hgraph : ∀ z ∈ V, Fin.snoc z (g z) ∈ U) : HasFDerivWithinAt (fun (z : Fin m → ℝ) => f (Fin.snoc z (g z))) ((fderivWithin ℝ f U (Fin.snoc x (g x))).comp (helperForProposition_6_17_DGx g V x)) V x

Helper for Proposition 6.17: chain-rule derivative for the constrained composition z ↦ f (z, g z) within V.

theorem helperForProposition_6_17_DGxApplyBasis {m : ℕ} {V : Set (Fin m → ℝ)} {g : (Fin m → ℝ) → ℝ} {x : Fin m → ℝ} (j : Fin m) : (helperForProposition_6_17_DGx g V x) (Pi.single j 1) = Fin.snoc (Pi.single j 1) (partialDerivWithin g V x j)

Helper for Proposition 6.17: evaluate DGx on the jth basis vector.

theorem helperForProposition_6_17_snocBasisDecomposition {m : ℕ} {V : Set (Fin m → ℝ)} {g : (Fin m → ℝ) → ℝ} {x : Fin m → ℝ} (j : Fin m) : Fin.snoc (Pi.single j 1) (partialDerivWithin g V x j) = Pi.single j.castSucc 1 + partialDerivWithin g V x j • Pi.single (Fin.last m) 1

Helper for Proposition 6.17: decompose Fin.snoc of a basis direction into the castSucc and last coordinate basis vectors.

theorem helperForProposition_6_17_linearIdentity {m : ℕ} {U : Set (Fin (m + 1) → ℝ)} {V : Set (Fin m → ℝ)} {f : (Fin (m + 1) → ℝ) → ℝ} {g : (Fin m → ℝ) → ℝ} (hVopen : IsOpen V) (hf : DifferentiableOn ℝ f U) (hg : DifferentiableOn ℝ g V) (hgraph : ∀ z ∈ V, Fin.snoc z (g z) ∈ U) (hconstraint : ∀ z ∈ V, f (Fin.snoc z (g z)) = 0) (j : Fin m) (x : Fin m → ℝ) (hx : x ∈ V) : partialDerivWithin f U (Fin.snoc x (g x)) j.castSucc + partialDerivWithin f U (Fin.snoc x (g x)) (Fin.last m) * partialDerivWithin g V x j = 0

Helper for Proposition 6.17: linear identity obtained by differentiating the constraint f (x, g x) = 0 within V.

theorem helperForProposition_6_17_solveForPartialG (A B C : ℝ) (hLinear : A + B * C = 0) (hB : B ≠ 0) : C = -A / B

Helper for Proposition 6.17: solve A + B*C = 0 for C when B ≠ 0.

theorem implicitDifferentiationForImplicitConstraint (m : ℕ) (U : Set (Fin (m + 1) → ℝ)) (f : (Fin (m + 1) → ℝ) → ℝ) (V : Set (Fin m → ℝ)) (g : (Fin m → ℝ) → ℝ) (hf : DifferentiableOn ℝ f U) (hVopen : IsOpen V) (hg : DifferentiableOn ℝ g V) (hgraph : ∀ x ∈ V, Fin.snoc x (g x) ∈ U) (hconstraint : ∀ x ∈ V, f (Fin.snoc x (g x)) = 0) : (∀ (j : Fin m), ∀ x ∈ V, partialDerivWithin f U (Fin.snoc x (g x)) j.castSucc + partialDerivWithin f U (Fin.snoc x (g x)) (Fin.last m) * partialDerivWithin g V x j = 0) ∧ ∀ (j : Fin m), ∀ x ∈ V, partialDerivWithin f U (Fin.snoc x (g x)) (Fin.last m) ≠ 0 → partialDerivWithin g V x j = -partialDerivWithin f U (Fin.snoc x (g x)) j.castSucc / partialDerivWithin f U (Fin.snoc x (g x)) (Fin.last m)

Proposition 6.17 (Implicit differentiation for an implicit constraint): in ambient coordinates with m free variables and one dependent coordinate (book's n = m + 1), if f : ℝ^(m+1) → ℝ and g : ℝ^m → ℝ are differentiable on open sets U and V, a ∈ U satisfies f a = 0 and nonvanishing last partial derivative at a, and f (x, g x) = 0 for all x ∈ V with (x, g x) ∈ U, then for each coordinate j and each x ∈ V one has ∂ⱼ f(x, g x) + ∂ₘ₊₁ f(x, g x) * ∂ⱼ g(x) = 0; equivalently, ∂ⱼ g(x) = -(∂ⱼ f(x, g x)) / (∂ₘ₊₁ f(x, g x)) whenever ∂ₘ₊₁ f(x, g x) ≠ 0.

theorem regularLevelSetAsLocalGraph (m : ℕ) (f : (Fin (m + 1) → ℝ) → ℝ) (x₀ : Fin (m + 1) → ℝ) (hf : ContDiff ℝ 1 f) (hx₀ : f x₀ = 0) : (∃ (j : Fin (m + 1)), partialDerivWithin f Set.univ x₀ j ≠ 0) → ∃ (j : Fin (m + 1)), partialDerivWithin f Set.univ x₀ j ≠ 0 ∧ ∃ (U : Set (Fin m → ℝ)), IsOpen U ∧ ∃ (W : Set (Fin (m + 1) → ℝ)), IsOpen W ∧ x₀ ∈ W ∧ ∃ (g : (Fin m → ℝ) → ℝ), DifferentiableOn ℝ g U ∧ {x : Fin (m + 1) → ℝ | x ∈ W ∧ f x = 0} = (fun (x' : Fin m → ℝ) => j.insertNth (g x') x') '' U

Definition 6.20 (Regular level set as a local graph): with ambient coordinates ℝ^(m+1) (so the book's ambient dimension parameter is n = m + 1), let f : ℝ^(m+1) → ℝ be continuously differentiable and let x₀ satisfy f x₀ = 0. If some coordinate partial derivative of f at x₀ is nonzero, then locally near x₀ the zero level set {x | f x = 0} is the graph of a differentiable function g : ℝ^m → ℝ, matching the book's ℝ^(n-1) parameter space.