One-dimensional derivatives on pi-types. #
theorem
hasDerivAt_update
{𝕜 : Type u_1}
{ι : Type u_2}
[DecidableEq ι]
[Fintype ι]
[NontriviallyNormedField 𝕜]
(x : ι → 𝕜)
(i : ι)
(y : 𝕜)
:
HasDerivAt (Function.update x i) (Pi.single i 1) y
theorem
hasDerivAt_single
{𝕜 : Type u_1}
{ι : Type u_2}
[DecidableEq ι]
[Fintype ι]
[NontriviallyNormedField 𝕜]
(i : ι)
(y : 𝕜)
:
HasDerivAt (Pi.single i) (Pi.single i 1) y
theorem
deriv_update
{𝕜 : Type u_1}
{ι : Type u_2}
[DecidableEq ι]
[Fintype ι]
[NontriviallyNormedField 𝕜]
(x : ι → 𝕜)
(i : ι)
(y : 𝕜)
:
deriv (Function.update x i) y = Pi.single i 1
theorem
deriv_single
{𝕜 : Type u_1}
{ι : Type u_2}
[DecidableEq ι]
[Fintype ι]
[NontriviallyNormedField 𝕜]
(i : ι)
(y : 𝕜)
: