Analysis II (Tao, 2022) -- Chapter 06 -- Section 04 -- Part 2

section Chap06section Section04

Helper for Theorem 6.4: in the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt branch, if one assumes canonicity of within-derivative witnesses for Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f at Unknown identifier `x0`x0, then the matrix identity follows.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_assumedCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hWitnessForm :
      DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
        ∃ L : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
          HasFDerivWithinAt (g ∘ f) L E x0 ∧
            LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
                L.toLinearMap =
              LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
                  (fderivWithin ℝ g F (f x0)).toLinearMap *
                LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
                  (fderivWithin ℝ f E x0).toLinearMap := by
    refine ⟨?_, ?_⟩
    · exact
        helperForTheorem_6_4_matrixForm_chainRule_differentiableWithin
          hMaps hf hg
    · refine
        ⟨(fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0), ?_, ?_⟩
      · exact
          helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives
            hMaps hf hg
      · simpa using
          (LinearMap.toMatrix_comp
            (Pi.basisFun ℝ (Fin n))
            (Pi.basisFun ℝ (Fin m))
            (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap
            (fderivWithin ℝ f E x0).toLinearMap)
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_witnessForm_and_canonicity
      hWitnessForm.1 hWitnessForm.2 hCanonicity

Helper for Theorem 6.4: in the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt branch, an assumed canonicity principle for within-derivative witnesses yields the full conclusion pair (within-set differentiability and matrix identity).

theorem helperForTheorem_6_4_matrixForm_chainRule_conclusion_of_not_uniqueDiff_of_assumedCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  refine ⟨?_, ?_⟩
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_differentiableWithin
        hMaps hf hg
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_assumedCanonicity
        hMaps hf hg hCanonicity

Helper for Theorem 6.4: adding explicit pointwise canonicity for within-derivative witnesses of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f yields the full matrix-form chain-rule conclusion.

theorem helperForTheorem_6_4_matrixForm_chainRule_with_pointCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hPointCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  by_cases hUnique : UniqueDiffWithinAt ℝ E x0
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_conclusion_of_uniqueDiff
        hMaps hf hg hUnique
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_conclusion_of_not_uniqueDiff_of_assumedCanonicity
        hMaps hf hg hPointCanonicity

Helper for Theorem 6.4: if either Unknown identifier `f`f or Unknown identifier `g`g admits zero as a within-derivative at the relevant basepoint, the matrix identity follows from the corresponding zero-derivative fallback branch.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero_f_or_g
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hZeroDerivFG :
      HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0 ∨
        HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  rcases hZeroDerivFG with hZeroDerivF | hZeroDerivG
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_from_fderivWithin_comp
        (helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_uniqueDiff_or_hasFDerivWithinAt_zero
          hMaps hf hg (Or.inr hZeroDerivF))
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero_right
        hMaps hf hZeroDerivG

Helper for Theorem 6.4: in the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt branch, proving the matrix identity reduces to the residual case where neither zero-derivative fallback applies for Unknown identifier `f`f or Unknown identifier `g`g.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_by_zeroFallbackSplit
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hResidual :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0 →
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0) →
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  by_cases hZeroDerivF : HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero_f_or_g
        hMaps hf hg (Or.inl hZeroDerivF)
  · by_cases hZeroDerivG :
        HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)
    · exact
        helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero_f_or_g
          hMaps hf hg (Or.inr hZeroDerivG)
    · exact hResidual hZeroDerivF hZeroDerivG

Helper for Theorem 6.4: proving the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt matrix identity can be reduced to supplying a canonicity generator for the residual branch where both zero-derivative fallbacks are excluded.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_residualCanonicityGenerator
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hResidualCanonicity :
      ¬ HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0 →
      ¬ HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0) →
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  refine
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_by_zeroFallbackSplit
      hMaps hf hg ?_
  intro hNotZeroDerivF hNotZeroDerivG
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_nonzeroFallbacks_of_canonicity
      hMaps hf hg hNotZeroDerivF hNotZeroDerivG
      (hResidualCanonicity hNotZeroDerivF hNotZeroDerivG)

Helper for Theorem 6.4: in the non-UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt branch, proving the matrix identity is reduced to providing pointwise canonicity of within-derivative witnesses for Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f at Unknown identifier `x0`x0.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_reducedToPointCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0)) :
    (∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
      HasFDerivWithinAt (g ∘ f) L1 E x0 →
      HasFDerivWithinAt (g ∘ f) L2 E x0 →
      L1 = L2) →
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  intro hPointCanonicity
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_assumedCanonicity
      hMaps hf hg hPointCanonicity

Helper for Theorem 6.4: pointwise canonicity of within-derivative witnesses for Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f at Unknown identifier `x0`x0 yields equality between the selected within-derivative and the composed selected within-derivatives.

theorem helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_pointCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hPointCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    fderivWithin ℝ (g ∘ f) E x0 =
      (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
  have hDerivSelected :
      HasFDerivWithinAt (g ∘ f) (fderivWithin ℝ (g ∘ f) E x0) E x0 := by
    exact (hg.comp x0 hf hMaps).hasFDerivWithinAt
  have hDerivComp :
      HasFDerivWithinAt (g ∘ f)
        ((fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0)) E x0 := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives
        hMaps hf hg
  exact
    helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_twoHasFDerivWithinAt_witnesses_and_canonicity
      hDerivSelected hDerivComp hPointCanonicity

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_pointCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hPointCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  have hcomp :
      fderivWithin ℝ (g ∘ f) E x0 =
        (fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0) := by
    exact
      helperForTheorem_6_4_matrixForm_chainRule_fderivWithin_comp_of_pointCanonicity
        hMaps hf hg hPointCanonicity
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_fderivWithin_comp
      hcomp

Helper for Theorem 6.4: if either Unknown identifier `f`f has zero within-derivative at Unknown identifier `x0`x0 or Unknown identifier `g`g has zero within-derivative at Unknown identifier `f`f x0, then the matrix identity follows from the corresponding zero-derivative branch.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_zeroDerivativeFallback
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hZeroDeriv :
      HasFDerivWithinAt f (0 : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ)) E x0 ∨
      HasFDerivWithinAt g (0 : (Fin m → ℝ) →L[ℝ] (Fin p → ℝ)) F (f x0)) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  rcases hZeroDeriv with hZeroDerivF | hZeroDerivG
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero
        hMaps hg hZeroDerivF
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_hasFDerivWithinAt_zero_right
        hMaps hf hZeroDerivG

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_pointCanonicity
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hPointCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_reducedToPointCanonicity
      hMaps hf hg hPointCanonicity

Helper for Theorem 6.4: remaining matrix-identity branch under ¬UniqueDiffWithinAt ℝ sorry sorry : Prop¬ UniqueDiffWithinAt ℝ Unknown identifier `E`E Unknown identifier `x0`x0, assuming a supplied pointwise canonicity principle for within-derivative witnesses of Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f.

theorem helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (unused variable `hx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hx0 : x0 ∈ E)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (unused variable `hfx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hfx0 : f x0 ∈ F)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (unused variable `hNotUnique`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hNotUnique : ¬ UniqueDiffWithinAt ℝ E x0)
    (hPointCanonicity :
      ∀ L1 L2 : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L1 E x0 →
        HasFDerivWithinAt (g ∘ f) L2 E x0 →
        L1 = L2) :
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
        (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap *
    LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
          (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_matrixIdentity_of_not_uniqueDiff_of_pointCanonicity
      hMaps hf hg hPointCanonicity

Helper for Theorem 6.4: with the exact hypotheses of matrixForm_chainRule {n m p : ℕ} {E : Set (Fin n → ℝ)} {F : Set (Fin m → ℝ)} {f : (Fin n → ℝ) → Fin m → ℝ} {g : (Fin m → ℝ) → Fin p → ℝ} {x0 : Fin n → ℝ} (hMaps : Set.MapsTo f E F) (hx0 : x0 ∈ E) (hf : DifferentiableWithinAt ℝ f E x0) (hfx0 : f x0 ∈ F) (hg : DifferentiableWithinAt ℝ g F (f x0)) (hUnique : UniqueDiffWithinAt ℝ E x0) : DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧ (LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))) ↑(fderivWithin ℝ (g ∘ f) E x0) = (LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))) ↑(fderivWithin ℝ g F (f x0)) * (LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))) ↑(fderivWithin ℝ f E x0)matrixForm_chainRule and an added UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt hypothesis, the full conclusion follows.

theorem helperForTheorem_6_4_matrixForm_chainRule_conclusion_with_uniqueDiff_mainHypotheses
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_conclusion_of_uniqueDiff
      hMaps hf hg hUnique

Helper for Theorem 6.4: a repaired variant of the theorem statement that adds UniqueDiffWithinAt.{u_1, u_2} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : PropUniqueDiffWithinAt to ensure canonicity of within-derivatives.

theorem helperForTheorem_6_4_matrixForm_chainRule_with_uniqueDiff
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_conclusion_with_uniqueDiff_mainHypotheses
      hMaps hf hg hUnique

Helper for Theorem 6.4: a witness-form chain-rule conclusion that avoids non-canonical selection of fderivWithin.{u_4, u_5, u_6} (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) (x : E) : E →L[𝕜] FfderivWithin for Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f.

theorem helperForTheorem_6_4_matrixForm_chainRule_witnessForm
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (hg : DifferentiableWithinAt ℝ g F (f x0)) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
      ∃ L : (Fin n → ℝ) →L[ℝ] (Fin p → ℝ),
        HasFDerivWithinAt (g ∘ f) L E x0 ∧
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
              L.toLinearMap =
            LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
                (fderivWithin ℝ g F (f x0)).toLinearMap *
              LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
                (fderivWithin ℝ f E x0).toLinearMap := by
  refine ⟨?_, ?_⟩
  · exact
      helperForTheorem_6_4_matrixForm_chainRule_differentiableWithin
        hMaps hf hg
  · refine
      ⟨(fderivWithin ℝ g F (f x0)).comp (fderivWithin ℝ f E x0), ?_, ?_⟩
    · exact
        helperForTheorem_6_4_matrixForm_chainRule_hasFDerivWithinAt_comp_of_selectedWithinDerivatives
          hMaps hf hg
    · simpa using
        (LinearMap.toMatrix_comp
          (Pi.basisFun ℝ (Fin n))
          (Pi.basisFun ℝ (Fin m))
          (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ g F (f x0)).toLinearMap
          (fderivWithin ℝ f E x0).toLinearMap)

Theorem 6.4: (Matrix form of the chain rule) let and , , and . Assume Unknown identifier `x₀`sorry ∈ sorry : Propx₀ ∈ Unknown identifier `E`E, Unknown identifier `f`sorry ∈ sorry : Propf x₀ ∈ Unknown identifier `F`F, Unknown identifier `f`f is differentiable within Unknown identifier `E`E at Unknown identifier `x₀`x₀, Unknown identifier `g`g is differentiable within Unknown identifier `F`F at Unknown identifier `f`f x₀, and Unknown identifier `f`f maps Unknown identifier `E`E into Unknown identifier `F`F. Assume also UniqueDiffWithinAt ℝ sorry sorry : PropUniqueDiffWithinAt ℝ Unknown identifier `E`E Unknown identifier `x₀`x₀ so the selected within-derivative is canonical. Then Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f is differentiable within Unknown identifier `E`E at Unknown identifier `x₀`x₀, and its within-derivative matrix satisfies .

theorem matrixForm_chainRule
    {n m p : ℕ}
    {E : Set (Fin n → ℝ)}
    {F : Set (Fin m → ℝ)}
    {f : (Fin n → ℝ) → (Fin m → ℝ)}
    {g : (Fin m → ℝ) → (Fin p → ℝ)}
    {x0 : Fin n → ℝ}
    (hMaps : Set.MapsTo f E F)
    (unused variable `hx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hx0 : x0 ∈ E)
    (hf : DifferentiableWithinAt ℝ f E x0)
    (unused variable `hfx0`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hfx0 : f x0 ∈ F)
    (hg : DifferentiableWithinAt ℝ g F (f x0))
    (hUnique : UniqueDiffWithinAt ℝ E x0) :
    DifferentiableWithinAt ℝ (g ∘ f) E x0 ∧
      LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin p))
          (fderivWithin ℝ (g ∘ f) E x0).toLinearMap =
        LinearMap.toMatrix (Pi.basisFun ℝ (Fin m)) (Pi.basisFun ℝ (Fin p))
            (fderivWithin ℝ g F (f x0)).toLinearMap *
          LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))
            (fderivWithin ℝ f E x0).toLinearMap := by
  exact
    helperForTheorem_6_4_matrixForm_chainRule_with_uniqueDiff
      hMaps hf hg hUnique

end Section04end Chap06