Analysis II (Tao, 2022) -- Chapter 06 -- Section 02

section Chap06section Section02

Definition 6.7 (Derivative in one variable): let failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `E`E ⊆ ℝ, , and Unknown identifier `x₀`sorry ∈ sorry : Propx₀ ∈ Unknown identifier `E`E. A real number Unknown identifier `L`L is the derivative of Unknown identifier `f`f at Unknown identifier `x₀`x₀ iff (sorry - sorry) / (sorry - sorry) : ?m.15(Unknown identifier `f`f x - Unknown identifier `f`f x₀) / (Unknown identifier `x`x - Unknown identifier `x₀`x₀) tends to Unknown identifier `L`L as Unknown identifier `x`sorry → sorry : Sort (imax u_1 u_2)x → Unknown identifier `x₀`x₀ with Unknown identifier `x`sorry ∈ sorry \ sorry : Propx ∈ Unknown identifier `E`E \ overloaded, errors 2:8 Unknown identifier `x₀` invalid {...} notation, expected type is not known{x₀}.

def HasDerivativeInOneVariableAt (E : Set ℝ) (f : E → ℝ) (x₀ : E) (L : ℝ) : Prop := Filter.Tendsto (fun x : E => (f x - f x₀) / ((x : ℝ) - (x₀ : ℝ))) (nhdsWithin x₀ {x : E | (x : ℝ) ≠ (x₀ : ℝ)}) (nhds L)

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

lemma 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| := by set d : ℝ := (x : ℝ) - (x₀ : ℝ) have hd : d ≠ 0 := by exact sub_ne_zero.mpr hx calc |f x - (f x₀ + L * ((x : ℝ) - (x₀ : ℝ)))| / |(x : ℝ) - (x₀ : ℝ)| = |(f x - (f x₀ + L * ((x : ℝ) - (x₀ : ℝ)))) / ((x : ℝ) - (x₀ : ℝ))| := by rw [← abs_div] _ = |((f x - f x₀) / ((x : ℝ) - (x₀ : ℝ))) - L| := by congr 1 field_simp [hd, d] ring

Helper for Lemma 6.4: on the punctured nhdsWithin.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) : Filter XnhdsWithin filter, points are eventually different from the basepoint.

lemma helperForLemma_6_4_eventually_ne_basepoint_on_puncturedFilter (E : Set ℝ) (x₀ : E) : ∀ᶠ x : E in nhdsWithin (X := E) x₀ {x : E | (x : ℝ) ≠ (x₀ : ℝ)}, (x : ℝ) ≠ (x₀ : ℝ) := by exact self_mem_nhdsWithin

Helper for Lemma 6.4: eventual equality between the target error ratio and the absolute form |sorry - sorry| : ?m.1|Unknown identifier `quotient`quotient - Unknown identifier `L`L| on the punctured filter.

lemma 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|) := by filter_upwards [helperForLemma_6_4_eventually_ne_basepoint_on_puncturedFilter E x₀] with x hx simpa using helperForLemma_6_4_pointwise_absErrorRatio_eq_absQuotientSub E f x₀ L x hx

Lemma 6.4: let failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `E`E ⊆ ℝ, , Unknown identifier `x₀`sorry ∈ sorry : Propx₀ ∈ Unknown identifier `E`E a limit point of Unknown identifier `E`E, and failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `L`L ∈ ℝ. Then (sorry - sorry) / (sorry - sorry) → sorry : Sort (imax u_3 u_8)(Unknown identifier `f`f x - Unknown identifier `f`f x₀) / (Unknown identifier `x`x - Unknown identifier `x₀`x₀) → Unknown identifier `L`L as Unknown identifier `x`sorry → sorry : Sort (imax u_1 u_2)x → Unknown identifier `x₀`x₀ in Unknown identifier `E`sorry \ sorry : ?m.1E \ overloaded, errors 2:2 Unknown identifier `x₀` invalid {...} notation, expected type is not known{x₀} iff |sorry - (sorry + sorry)| / |sorry - sorry| → sorry : Sort (imax u_3 u_10)|Unknown identifier `f`f x - (Unknown identifier `f`f x₀ + Unknown identifier `L`L (x - x₀))| / |Unknown identifier `x`x - Unknown identifier `x₀`x₀| → failed to synthesize OfNat (Sort ?u.709476) 0 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is Sort ?u.709476 due to the absence of the instance above Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.0 on the same punctured domain.

lemma hasDerivativeInOneVariableAt_iff_tendsto_normErrorRatio_zero (E : Set ℝ) (f : E → ℝ) (x₀ : E) (L : ℝ) (unused variable `hlimit` Note: This linter can be disabled with `set_option linter.unusedVariables false`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 : ℝ)) := by let punctured : Set E := {x : E | (x : ℝ) ≠ (x₀ : ℝ)} let quotient : E → ℝ := fun x => (f x - f x₀) / ((x : ℝ) - (x₀ : ℝ)) let errorRatio : E → ℝ := fun x => |f x - (f x₀ + L * ((x : ℝ) - (x₀ : ℝ)))| / |(x : ℝ) - (x₀ : ℝ)| have hEventualEq : errorRatio =ᶠ[nhdsWithin x₀ punctured] (fun x : E => |quotient x - L|) := by simpa [punctured, quotient, errorRatio] using helperForLemma_6_4_eventuallyEq_errorRatio_absSubForm E f x₀ L constructor · intro hDeriv have hQuotient : Filter.Tendsto quotient (nhdsWithin x₀ punctured) (nhds L) := by simpa [HasDerivativeInOneVariableAt, punctured, quotient] using hDeriv have hNormSub : Filter.Tendsto (fun x : E => ‖quotient x - L‖) (nhdsWithin x₀ punctured) (nhds (0 : ℝ)) := by exact (tendsto_iff_norm_sub_tendsto_zero).1 hQuotient have hAbsSub : Filter.Tendsto (fun x : E => |quotient x - L|) (nhdsWithin x₀ punctured) (nhds (0 : ℝ)) := by simpa [Real.norm_eq_abs] using hNormSub have hErrorRatio : Filter.Tendsto errorRatio (nhdsWithin x₀ punctured) (nhds (0 : ℝ)) := by exact Filter.Tendsto.congr' hEventualEq.symm hAbsSub simpa [punctured, errorRatio] using hErrorRatio · intro hError have hErrorRatio : Filter.Tendsto errorRatio (nhdsWithin x₀ punctured) (nhds (0 : ℝ)) := by simpa [punctured, errorRatio] using hError have hAbsSub : Filter.Tendsto (fun x : E => |quotient x - L|) (nhdsWithin x₀ punctured) (nhds (0 : ℝ)) := by exact Filter.Tendsto.congr' hEventualEq hErrorRatio have hNormSub : Filter.Tendsto (fun x : E => ‖quotient x - L‖) (nhdsWithin x₀ punctured) (nhds (0 : ℝ)) := by simpa [Real.norm_eq_abs] using hAbsSub have hQuotient : Filter.Tendsto quotient (nhdsWithin x₀ punctured) (nhds L) := by exact (tendsto_iff_norm_sub_tendsto_zero).2 hNormSub simpa [HasDerivativeInOneVariableAt, punctured, quotient] using hQuotient

Definition 6.8 (Differentiability): let failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `E`E ⊆ ℝ^Unknown identifier `n`n, , and Unknown identifier `x₀`sorry ∈ sorry : Propx₀ ∈ Unknown identifier `E`E be a limit point of Unknown identifier `E`E. For a linear map , Unknown identifier `f`f is differentiable at Unknown identifier `x₀`x₀ with derivative Unknown identifier `L`L when sorry → sorry : Sort (imax u_1 u_2)‖Unknown identifier `f`f x - (Unknown identifier `f`f x₀ + Unknown identifier `L`L (x - x₀))‖ / ‖Unknown identifier `x`x - Unknown identifier `x₀`x₀‖ → failed to synthesize OfNat (Sort ?u.717788) 0 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is Sort ?u.717788 due to the absence of the instance above Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.0 as Unknown identifier `x`sorry → sorry : Sort (imax u_1 u_2)x → Unknown identifier `x₀`x₀ with Unknown identifier `x`sorry ∈ sorry \ sorry : Propx ∈ Unknown identifier `E`E \ overloaded, errors 2:8 Unknown identifier `x₀` invalid {...} notation, expected type is not known{x₀}, using the Euclidean norm.

def HasDerivativeInSeveralVariablesAt (n m : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (f : E → EuclideanSpace ℝ (Fin m)) (x₀ : E) (L : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : Prop := ((x₀ : EuclideanSpace ℝ (Fin n)) ∈ closure (E \ {(x₀ : EuclideanSpace ℝ (Fin n))})) ∧ Filter.Tendsto (fun x : E => ‖f x - (f x₀ + L ((x : EuclideanSpace ℝ (Fin n)) - (x₀ : EuclideanSpace ℝ (Fin n))))‖ / ‖(x : EuclideanSpace ℝ (Fin n)) - (x₀ : EuclideanSpace ℝ (Fin n))‖) (nhdsWithin x₀ {x : E | x ≠ x₀}) (nhds (0 : ℝ))

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

lemma helperForProposition_6_8_memClosure_univ_diff_singleton (x₀ : EuclideanSpace ℝ (Fin 2)) : x₀ ∈ closure ((Set.univ : Set (EuclideanSpace ℝ (Fin 2))) \ {x₀}) := by have hdense : Dense ({x₀}ᶜ : Set (EuclideanSpace ℝ (Fin 2))) := dense_compl_singleton x₀ have hclosure : closure ({x₀}ᶜ : Set (EuclideanSpace ℝ (Fin 2))) = Set.univ := hdense.closure_eq have hmem : x₀ ∈ closure ({x₀}ᶜ : Set (EuclideanSpace ℝ (Fin 2))) := by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hclosure] have hset : ((Set.univ : Set (EuclideanSpace ℝ (Fin 2))) \ {x₀}) = ({x₀}ᶜ : Set (EuclideanSpace ℝ (Fin 2))) := by ext x simp try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hset] using hmem

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

lemma helperForProposition_6_8_f_eq_coordinateSquare_onSubtypeUniv (f : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} → EuclideanSpace ℝ (Fin 2)) (hf₀ : ∀ p : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}, (f p) 0 = ((p : EuclideanSpace ℝ (Fin 2)) 0) ^ (2 : ℕ)) (hf₁ : ∀ p : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}, (f p) 1 = ((p : EuclideanSpace ℝ (Fin 2)) 1) ^ (2 : ℕ)) (p : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}) : f p = (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => ((p : EuclideanSpace ℝ (Fin 2)) i) ^ (2 : ℕ)) := by ext i fin_cases i · simp [hf₀] · simp [hf₁]

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

lemma helperForProposition_6_8_hasFDerivAt_coordinateSquare_at_x0 (x₀ : EuclideanSpace ℝ (Fin 2)) (hx₀₀ : x₀ 0 = (1 : ℝ)) (hx₀₁ : x₀ 1 = (2 : ℝ)) (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) (hL₀ : ∀ v : EuclideanSpace ℝ (Fin 2), (L v) 0 = (2 : ℝ) * v 0) (hL₁ : ∀ v : EuclideanSpace ℝ (Fin 2), (L v) 1 = (4 : ℝ) * v 1) : HasFDerivAt (fun x : EuclideanSpace ℝ (Fin 2) => (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ))) (LinearMap.toContinuousLinearMap L) x₀ := by let φ' : Fin 2 → EuclideanSpace ℝ (Fin 2) →L[ℝ] ℝ := fun i => ((2 : ℝ) * x₀ i) • (EuclideanSpace.proj (𝕜 := ℝ) (ι := Fin 2) i) have hφ : HasFDerivAt (fun x : EuclideanSpace ℝ (Fin 2) => (fun i : Fin 2 => (x i) ^ (2 : ℕ))) (ContinuousLinearMap.pi φ') x₀ := by refine (hasFDerivAt_pi).2 ?_ intro i simpa [φ', pow_one, one_mul, smul_smul, mul_assoc] using ((EuclideanSpace.proj (𝕜 := ℝ) (ι := Fin 2) i).hasFDerivAt.pow (2 : ℕ) (x := x₀)) have hsymm : HasFDerivAt ((EuclideanSpace.equiv (Fin 2) ℝ).symm : (Fin 2 → ℝ) → EuclideanSpace ℝ (Fin 2)) (EuclideanSpace.equiv (Fin 2) ℝ).symm.toContinuousLinearMap ((fun i : Fin 2 => (x₀ i) ^ (2 : ℕ))) := (EuclideanSpace.equiv (Fin 2) ℝ).symm.toContinuousLinearMap.hasFDerivAt have hDerivM : HasFDerivAt (fun x : EuclideanSpace ℝ (Fin 2) => (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ))) ((EuclideanSpace.equiv (Fin 2) ℝ).symm.toContinuousLinearMap.comp (ContinuousLinearMap.pi φ')) x₀ := by simpa [Function.comp] using hsymm.comp x₀ hφ have hCoeff0 : (2 : ℝ) * x₀ 0 = 2 := by nlinarith [hx₀₀] have hCoeff1 : (2 : ℝ) * x₀ 1 = 4 := by nlinarith [hx₀₁] have hLext : (LinearMap.toContinuousLinearMap L) = ((EuclideanSpace.equiv (Fin 2) ℝ).symm.toContinuousLinearMap.comp (ContinuousLinearMap.pi φ')) := by ext v i fin_cases i · simp [φ', hL₀, hCoeff0] · simp [φ', hL₁, hCoeff1] simpa [hLext] using hDerivM

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

lemma 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 i) ^ (2 : ℕ))) (LinearMap.toContinuousLinearMap L) x₀) : Filter.Tendsto (fun x : EuclideanSpace ℝ (Fin 2) => ‖(EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ)) - ((EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x₀ i) ^ (2 : ℕ)) + L (x - x₀))‖ / ‖x - x₀‖) (nhdsWithin x₀ {x : EuclideanSpace ℝ (Fin 2) | x ≠ x₀}) (nhds (0 : ℝ)) := by have hLittle : (fun x : EuclideanSpace ℝ (Fin 2) => (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ)) - ((EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x₀ i) ^ (2 : ℕ)) + L (x - x₀))) =o[nhds x₀] (fun x : EuclideanSpace ℝ (Fin 2) => x - x₀) := by simpa [LinearMap.map_sub, sub_eq_add_neg, add_assoc, add_comm, add_left_comm] using hFDeriv.isLittleO have hLittleWithin : (fun x : EuclideanSpace ℝ (Fin 2) => (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ)) - ((EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x₀ i) ^ (2 : ℕ)) + L (x - x₀))) =o[nhdsWithin x₀ {x : EuclideanSpace ℝ (Fin 2) | x ≠ x₀}] (fun x : EuclideanSpace ℝ (Fin 2) => x - x₀) := hLittle.mono nhdsWithin_le_nhds have hNormLittle : (fun x : EuclideanSpace ℝ (Fin 2) => ‖(EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ)) - ((EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x₀ i) ^ (2 : ℕ)) + L (x - x₀))‖) =o[nhdsWithin x₀ {x : EuclideanSpace ℝ (Fin 2) | x ≠ x₀}] (fun x : EuclideanSpace ℝ (Fin 2) => x - x₀) := hLittleWithin.norm_left have hNormNormLittle : (fun x : EuclideanSpace ℝ (Fin 2) => ‖(EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ)) - ((EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x₀ i) ^ (2 : ℕ)) + L (x - x₀))‖) =o[nhdsWithin x₀ {x : EuclideanSpace ℝ (Fin 2) | x ≠ x₀}] (fun x : EuclideanSpace ℝ (Fin 2) => ‖x - x₀‖) := hNormLittle.norm_right simpa using hNormNormLittle.tendsto_div_nhds_zero

Helper for Proposition 6.8: punctured neighborhood filters on Subtype sorry : Sort (max 1 u_1)Subtype Unknown identifier `univ`univ agree with the ambient punctured filter via coercion.

lemma helperForProposition_6_8_nhdsWithin_puncturedSubtypeUniv_eq_comap (x₀ : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}) : nhdsWithin x₀ {x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} | x ≠ x₀} = Filter.comap (fun x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} => (x : EuclideanSpace ℝ (Fin 2))) (nhdsWithin (x₀ : EuclideanSpace ℝ (Fin 2)) {x : EuclideanSpace ℝ (Fin 2) | x ≠ (x₀ : EuclideanSpace ℝ (Fin 2))}) := by have hImage : (Subtype.val '' ({x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} | x ≠ x₀})) = ({x : EuclideanSpace ℝ (Fin 2) | x ≠ (x₀ : EuclideanSpace ℝ (Fin 2))}) := by ext x constructor · rintro ⟨y, hy, rfl⟩ intro hEq exact hy (Subtype.ext hEq) · intro hx have hxUniv : x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2))) := by simp let xSub : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} := ⟨x, hxUniv⟩ have hx' : xSub ≠ x₀ := by intro hSub exact hx (congrArg Subtype.val hSub) exact ⟨xSub, hx', rfl⟩ simpa [hImage] using (nhdsWithin_subtype (Set.univ : Set (EuclideanSpace ℝ (Fin 2))) x₀ ({x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} | x ≠ x₀}))

Proposition 6.8: if is given by , then Unknown identifier `f`f is differentiable at Unknown identifier `x₀`sorry = (1, 2) : Propx₀ = (1, 2) with derivative .

theorem hasDerivativeInSeveralVariablesAt_coordinateSquare_at_one_two (x₀ : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}) (hx₀₀ : (x₀ : EuclideanSpace ℝ (Fin 2)) 0 = (1 : ℝ)) (hx₀₁ : (x₀ : EuclideanSpace ℝ (Fin 2)) 1 = (2 : ℝ)) (f : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} → EuclideanSpace ℝ (Fin 2)) (hf₀ : ∀ p : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}, (f p) 0 = ((p : EuclideanSpace ℝ (Fin 2)) 0) ^ (2 : ℕ)) (hf₁ : ∀ p : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}, (f p) 1 = ((p : EuclideanSpace ℝ (Fin 2)) 1) ^ (2 : ℕ)) (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) (hL₀ : ∀ v : EuclideanSpace ℝ (Fin 2), (L v) 0 = (2 : ℝ) * v 0) (hL₁ : ∀ v : EuclideanSpace ℝ (Fin 2), (L v) 1 = (4 : ℝ) * v 1) : HasDerivativeInSeveralVariablesAt 2 2 (Set.univ : Set (EuclideanSpace ℝ (Fin 2))) f x₀ L := by refine And.intro ?_ ?_ · exact helperForProposition_6_8_memClosure_univ_diff_singleton (x₀ := (x₀ : EuclideanSpace ℝ (Fin 2))) · let coordinateSquare : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) := fun x => (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => (x i) ^ (2 : ℕ)) let coordinateSquareSubtype : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} → EuclideanSpace ℝ (Fin 2) := fun x => coordinateSquare (x : EuclideanSpace ℝ (Fin 2)) have hFDeriv : HasFDerivAt coordinateSquare (LinearMap.toContinuousLinearMap L) (x₀ : EuclideanSpace ℝ (Fin 2)) := helperForProposition_6_8_hasFDerivAt_coordinateSquare_at_x0 (x₀ := (x₀ : EuclideanSpace ℝ (Fin 2))) hx₀₀ hx₀₁ L hL₀ hL₁ have hAmbientTendsto : Filter.Tendsto (fun x : EuclideanSpace ℝ (Fin 2) => ‖coordinateSquare x - (coordinateSquare (x₀ : EuclideanSpace ℝ (Fin 2)) + L (x - (x₀ : EuclideanSpace ℝ (Fin 2))))‖ / ‖x - (x₀ : EuclideanSpace ℝ (Fin 2))‖) (nhdsWithin (x₀ : EuclideanSpace ℝ (Fin 2)) {x : EuclideanSpace ℝ (Fin 2) | x ≠ (x₀ : EuclideanSpace ℝ (Fin 2))}) (nhds (0 : ℝ)) := by simpa [coordinateSquare] using helperForProposition_6_8_tendsto_errorRatio_on_puncturedAmbient (x₀ := (x₀ : EuclideanSpace ℝ (Fin 2))) (L := L) hFDeriv have hSubtypeTendsto : Filter.Tendsto (fun x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} => ‖coordinateSquareSubtype x - (coordinateSquareSubtype x₀ + L ((x : EuclideanSpace ℝ (Fin 2)) - (x₀ : EuclideanSpace ℝ (Fin 2))))‖ / ‖(x : EuclideanSpace ℝ (Fin 2)) - (x₀ : EuclideanSpace ℝ (Fin 2))‖) (nhdsWithin x₀ {x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} | x ≠ x₀}) (nhds (0 : ℝ)) := by rw [helperForProposition_6_8_nhdsWithin_puncturedSubtypeUniv_eq_comap (x₀ := x₀)] exact hAmbientTendsto.comp Filter.tendsto_comap have hfEqAtX : ∀ x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))}, f x = coordinateSquareSubtype x := by intro x simpa [coordinateSquareSubtype, coordinateSquare] using helperForProposition_6_8_f_eq_coordinateSquare_onSubtypeUniv f hf₀ hf₁ x have hTargetEq : (fun x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} => ‖f x - (f x₀ + L ((x : EuclideanSpace ℝ (Fin 2)) - (x₀ : EuclideanSpace ℝ (Fin 2))))‖ / ‖(x : EuclideanSpace ℝ (Fin 2)) - (x₀ : EuclideanSpace ℝ (Fin 2))‖) = (fun x : {x : EuclideanSpace ℝ (Fin 2) // x ∈ (Set.univ : Set (EuclideanSpace ℝ (Fin 2)))} => ‖coordinateSquareSubtype x - (coordinateSquareSubtype x₀ + L ((x : EuclideanSpace ℝ (Fin 2)) - (x₀ : EuclideanSpace ℝ (Fin 2))))‖ / ‖(x : EuclideanSpace ℝ (Fin 2)) - (x₀ : EuclideanSpace ℝ (Fin 2))‖) := by funext x simp [hfEqAtX x, hfEqAtX x₀] rw [hTargetEq] exact hSubtypeTendsto

Lemma 6.5 (Uniqueness of derivatives): if Unknown identifier `x₀`x₀ is an interior point of and both Unknown identifier `L₁`L₁ and Unknown identifier `L₂`L₂ satisfy the derivative error-ratio limit for at Unknown identifier `x₀`x₀, then the linear transformations coincide: Unknown identifier `L₁`sorry = sorry : PropL₁ = Unknown identifier `L₂`L₂.

theorem derivativeInSeveralVariables_unique (n m : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (f : E → EuclideanSpace ℝ (Fin m)) (x₀ : E) (hinterior : (x₀ : EuclideanSpace ℝ (Fin n)) ∈ 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₂ := by classical let fExt : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m) := fun x => if hx : x ∈ E then f ⟨x, hx⟩ else f x₀ have hHasFDerivWithin_of_custom : ∀ L : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m), HasDerivativeInSeveralVariablesAt n m E f x₀ L → HasFDerivWithinAt fExt (LinearMap.toContinuousLinearMap L) E (x₀ : EuclideanSpace ℝ (Fin n)) := by intro L hL let θ : EuclideanSpace ℝ (Fin n) → ℝ := fun x => ‖x - (x₀ : EuclideanSpace ℝ (Fin n))‖⁻¹ * ‖fExt x - fExt (x₀ : EuclideanSpace ℝ (Fin n)) - (LinearMap.toContinuousLinearMap L) (x - (x₀ : EuclideanSpace ℝ (Fin n)))‖ let ψ : E → ℝ := E.restrict θ have hψ_eq_target : ψ = (fun x : E => ‖f x - (f x₀ + L ((x : EuclideanSpace ℝ (Fin n)) - (x₀ : EuclideanSpace ℝ (Fin n))))‖ / ‖(x : EuclideanSpace ℝ (Fin n)) - (x₀ : EuclideanSpace ℝ (Fin n))‖) := by funext x simp [ψ, θ, fExt, div_eq_inv_mul, sub_eq_add_neg, add_assoc, add_comm] have hPunct : Filter.Tendsto ψ (nhdsWithin x₀ {x : E | x ≠ x₀}) (nhds (0 : ℝ)) := by rw [hψ_eq_target] exact hL.2 have hψx₀ : ψ x₀ = 0 := by simp [ψ, θ, fExt] have hPure : Filter.Tendsto ψ (pure x₀) (nhds (0 : ℝ)) := by simpa [hψx₀] using (tendsto_pure_nhds ψ x₀) have hSetNe : ({x : E | x ≠ x₀} : Set E) = ({x₀}ᶜ : Set E) := by ext x simp have hPunctCompl : Filter.Tendsto ψ (nhdsWithin x₀ ({x₀}ᶜ : Set E)) (nhds (0 : ℝ)) := by simpa [hSetNe] using hPunct have hSubtype : Filter.Tendsto ψ (nhds x₀) (nhds (0 : ℝ)) := by have hSup : Filter.Tendsto ψ (pure x₀ ⊔ nhdsWithin x₀ ({x₀}ᶜ : Set E)) (nhds (0 : ℝ)) := hPure.sup hPunctCompl simpa [pure_sup_nhdsNE] using hSup have hAmbient : Filter.Tendsto θ (nhdsWithin (x₀ : EuclideanSpace ℝ (Fin n)) E) (nhds (0 : ℝ)) := (tendsto_nhdsWithin_iff_subtype (s := E) (h := x₀.property) θ (nhds (0 : ℝ))).2 hSubtype rw [hasFDerivWithinAt_iff_tendsto] simpa [θ] using hAmbient have hFDeriv₁ : HasFDerivWithinAt fExt (LinearMap.toContinuousLinearMap L₁) E (x₀ : EuclideanSpace ℝ (Fin n)) := hHasFDerivWithin_of_custom L₁ hL₁ have hFDeriv₂ : HasFDerivWithinAt fExt (LinearMap.toContinuousLinearMap L₂) E (x₀ : EuclideanSpace ℝ (Fin n)) := hHasFDerivWithin_of_custom L₂ hL₂ have hUniqueDiff : UniqueDiffWithinAt ℝ E (x₀ : EuclideanSpace ℝ (Fin n)) := uniqueDiffWithinAt_of_mem_nhds (mem_interior_iff_mem_nhds.mp hinterior) have hEqCLM : LinearMap.toContinuousLinearMap L₁ = LinearMap.toContinuousLinearMap L₂ := hUniqueDiff.eq hFDeriv₁ hFDeriv₂ ext v i exact congrArg (fun T : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m) => (T v) i) hEqCLM
end Section02end Chap06