Derivatives on pi-types. #
theorem hasFDerivAt_update {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : (i : ι) → E i) {i : ι} (y : E i) :
HasFDerivAt (Function.update x i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y
theorem hasFDerivAt_single {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {i : ι} (y : E i) :
HasFDerivAt (Pi.single i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y
theorem fderiv_update {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : (i : ι) → E i) {i : ι} (y : E i) :
fderiv 𝕜 (Function.update x i) y = ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
theorem fderiv_single {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {i : ι} (y : E i) :