Calculus in inner product spaces #
In this file we prove that the inner product and square of the norm in an inner space are
infinitely β
-smooth. In order to state these results, we need a NormedSpace β E
instance. Though we can deduce this structure from InnerProductSpace π E
, this instance may be
not definitionally equal to some other βnaturalβ instance. So, we assume [NormedSpace β E]
.
We also prove that functions to a EuclideanSpace
are (higher) differentiable if and only if
their components are. This follows from the corresponding fact for finite product of normed spaces,
and from the equivalence of norms in finite dimensions.
TODO #
The last part of the file should be generalized to PiLp
.
def
fderivInnerCLM
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
(p : E Γ E)
:
Derivative of the inner product.
Equations
- fderivInnerCLM π p = β―.deriv p
Instances For
@[simp]
theorem
fderivInnerCLM_apply
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
(p x : E Γ E)
:
(fderivInnerCLM π p) x = inner p.1 x.2 + inner x.1 p.2
theorem
contDiff_inner
{π : Type u_1}
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{n : WithTop ββ}
:
theorem
contDiffAt_inner
{π : Type u_1}
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{p : E Γ E}
{n : WithTop ββ}
:
ContDiffAt β n (fun (p : E Γ E) => inner p.1 p.2) p
theorem
differentiable_inner
{π : Type u_1}
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
:
Differentiable β fun (p : E Γ E) => inner p.1 p.2
theorem
ContDiffWithinAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
{x : G}
{n : WithTop ββ}
(hf : ContDiffWithinAt β n f s x)
(hg : ContDiffWithinAt β n g s x)
:
ContDiffWithinAt β n (fun (x : G) => inner (f x) (g x)) s x
theorem
ContDiffAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{x : G}
{n : WithTop ββ}
(hf : ContDiffAt β n f x)
(hg : ContDiffAt β n g x)
:
ContDiffAt β n (fun (x : G) => inner (f x) (g x)) x
theorem
ContDiffOn.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
{n : WithTop ββ}
(hf : ContDiffOn β n f s)
(hg : ContDiffOn β n g s)
:
ContDiffOn β n (fun (x : G) => inner (f x) (g x)) s
theorem
ContDiff.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{n : WithTop ββ}
(hf : ContDiff β n f)
(hg : ContDiff β n g)
:
theorem
HasFDerivWithinAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{f' g' : G βL[β] E}
{s : Set G}
{x : G}
(hf : HasFDerivWithinAt f f' s x)
(hg : HasFDerivWithinAt g g' s x)
:
HasFDerivWithinAt (fun (t : G) => inner (f t) (g t)) ((fderivInnerCLM π (f x, g x)).comp (f'.prod g')) s x
theorem
HasStrictFDerivAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{f' g' : G βL[β] E}
{x : G}
(hf : HasStrictFDerivAt f f' x)
(hg : HasStrictFDerivAt g g' x)
:
HasStrictFDerivAt (fun (t : G) => inner (f t) (g t)) ((fderivInnerCLM π (f x, g x)).comp (f'.prod g')) x
theorem
HasFDerivAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{f' g' : G βL[β] E}
{x : G}
(hf : HasFDerivAt f f' x)
(hg : HasFDerivAt g g' x)
:
HasFDerivAt (fun (t : G) => inner (f t) (g t)) ((fderivInnerCLM π (f x, g x)).comp (f'.prod g')) x
theorem
HasDerivWithinAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{f g : β β E}
{f' g' : E}
{s : Set β}
{x : β}
(hf : HasDerivWithinAt f f' s x)
(hg : HasDerivWithinAt g g' s x)
:
theorem
HasDerivAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{f g : β β E}
{f' g' : E}
{x : β}
:
HasDerivAt f f' x β
HasDerivAt g g' x β HasDerivAt (fun (t : β) => inner (f t) (g t)) (inner (f x) g' + inner f' (g x)) x
theorem
DifferentiableWithinAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
{x : G}
(hf : DifferentiableWithinAt β f s x)
(hg : DifferentiableWithinAt β g s x)
:
DifferentiableWithinAt β (fun (x : G) => inner (f x) (g x)) s x
theorem
DifferentiableAt.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{x : G}
(hf : DifferentiableAt β f x)
(hg : DifferentiableAt β g x)
:
DifferentiableAt β (fun (x : G) => inner (f x) (g x)) x
theorem
DifferentiableOn.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
(hf : DifferentiableOn β f s)
(hg : DifferentiableOn β g s)
:
DifferentiableOn β (fun (x : G) => inner (f x) (g x)) s
theorem
Differentiable.inner
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
(hf : Differentiable β f)
(hg : Differentiable β g)
:
Differentiable β fun (x : G) => inner (f x) (g x)
theorem
fderiv_inner_apply
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{x : G}
(hf : DifferentiableAt β f x)
(hg : DifferentiableAt β g x)
(y : G)
:
theorem
deriv_inner_apply
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{f g : β β E}
{x : β}
(hf : DifferentiableAt β f x)
(hg : DifferentiableAt β g x)
:
theorem
contDiff_norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{n : WithTop ββ}
:
theorem
ContDiff.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{n : WithTop ββ}
(hf : ContDiff β n f)
:
theorem
ContDiffWithinAt.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
{x : G}
{n : WithTop ββ}
(hf : ContDiffWithinAt β n f s x)
:
ContDiffWithinAt β n (fun (y : G) => βf yβ ^ 2) s x
theorem
ContDiffAt.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{x : G}
{n : WithTop ββ}
(hf : ContDiffAt β n f x)
:
ContDiffAt β n (fun (x : G) => βf xβ ^ 2) x
theorem
contDiffAt_norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{n : WithTop ββ}
{x : E}
(hx : x β 0)
:
ContDiffAt β n norm x
theorem
ContDiffAt.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{x : G}
{n : WithTop ββ}
(hf : ContDiffAt β n f x)
(h0 : f x β 0)
:
ContDiffAt β n (fun (y : G) => βf yβ) x
theorem
ContDiffAt.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{x : G}
{n : WithTop ββ}
(hf : ContDiffAt β n f x)
(hg : ContDiffAt β n g x)
(hne : f x β g x)
:
ContDiffAt β n (fun (y : G) => dist (f y) (g y)) x
theorem
ContDiffWithinAt.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
{x : G}
{n : WithTop ββ}
(hf : ContDiffWithinAt β n f s x)
(h0 : f x β 0)
:
ContDiffWithinAt β n (fun (y : G) => βf yβ) s x
theorem
ContDiffWithinAt.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
{x : G}
{n : WithTop ββ}
(hf : ContDiffWithinAt β n f s x)
(hg : ContDiffWithinAt β n g s x)
(hne : f x β g x)
:
ContDiffWithinAt β n (fun (y : G) => dist (f y) (g y)) s x
theorem
ContDiffOn.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
{n : WithTop ββ}
(hf : ContDiffOn β n f s)
:
ContDiffOn β n (fun (y : G) => βf yβ ^ 2) s
theorem
ContDiffOn.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
{n : WithTop ββ}
(hf : ContDiffOn β n f s)
(h0 : β x β s, f x β 0)
:
ContDiffOn β n (fun (y : G) => βf yβ) s
theorem
ContDiffOn.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
{n : WithTop ββ}
(hf : ContDiffOn β n f s)
(hg : ContDiffOn β n g s)
(hne : β x β s, f x β g x)
:
ContDiffOn β n (fun (y : G) => dist (f y) (g y)) s
theorem
ContDiff.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{n : WithTop ββ}
(hf : ContDiff β n f)
(h0 : β (x : G), f x β 0)
:
theorem
ContDiff.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{n : WithTop ββ}
(hf : ContDiff β n f)
(hg : ContDiff β n g)
(hne : β (x : G), f x β g x)
:
theorem
hasStrictFDerivAt_norm_sq
{F : Type u_3}
[NormedAddCommGroup F]
[InnerProductSpace β F]
(x : F)
:
theorem
HasFDerivAt.norm_sq
{F : Type u_3}
[NormedAddCommGroup F]
[InnerProductSpace β F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{x : G}
{f : G β F}
{f' : G βL[β] F}
(hf : HasFDerivAt f f' x)
:
theorem
HasDerivAt.norm_sq
{F : Type u_3}
[NormedAddCommGroup F]
[InnerProductSpace β F]
{f : β β F}
{f' : F}
{x : β}
(hf : HasDerivAt f f' x)
:
theorem
HasFDerivWithinAt.norm_sq
{F : Type u_3}
[NormedAddCommGroup F]
[InnerProductSpace β F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{s : Set G}
{x : G}
{f : G β F}
{f' : G βL[β] F}
(hf : HasFDerivWithinAt f f' s x)
:
theorem
HasDerivWithinAt.norm_sq
{F : Type u_3}
[NormedAddCommGroup F]
[InnerProductSpace β F]
{f : β β F}
{f' : F}
{s : Set β}
{x : β}
(hf : HasDerivWithinAt f f' s x)
:
theorem
DifferentiableAt.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{x : G}
(hf : DifferentiableAt β f x)
:
DifferentiableAt β (fun (y : G) => βf yβ ^ 2) x
theorem
DifferentiableAt.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{x : G}
(hf : DifferentiableAt β f x)
(h0 : f x β 0)
:
DifferentiableAt β (fun (y : G) => βf yβ) x
theorem
DifferentiableAt.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{x : G}
(hf : DifferentiableAt β f x)
(hg : DifferentiableAt β g x)
(hne : f x β g x)
:
DifferentiableAt β (fun (y : G) => dist (f y) (g y)) x
theorem
Differentiable.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
(hf : Differentiable β f)
:
Differentiable β fun (y : G) => βf yβ ^ 2
theorem
Differentiable.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
(hf : Differentiable β f)
(h0 : β (x : G), f x β 0)
:
Differentiable β fun (y : G) => βf yβ
theorem
Differentiable.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
(hf : Differentiable β f)
(hg : Differentiable β g)
(hne : β (x : G), f x β g x)
:
Differentiable β fun (y : G) => dist (f y) (g y)
theorem
DifferentiableWithinAt.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
{x : G}
(hf : DifferentiableWithinAt β f s x)
:
DifferentiableWithinAt β (fun (y : G) => βf yβ ^ 2) s x
theorem
DifferentiableWithinAt.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
{x : G}
(hf : DifferentiableWithinAt β f s x)
(h0 : f x β 0)
:
DifferentiableWithinAt β (fun (y : G) => βf yβ) s x
theorem
DifferentiableWithinAt.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
{x : G}
(hf : DifferentiableWithinAt β f s x)
(hg : DifferentiableWithinAt β g s x)
(hne : f x β g x)
:
DifferentiableWithinAt β (fun (y : G) => dist (f y) (g y)) s x
theorem
DifferentiableOn.norm_sq
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
(hf : DifferentiableOn β f s)
:
DifferentiableOn β (fun (y : G) => βf yβ ^ 2) s
theorem
DifferentiableOn.norm
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f : G β E}
{s : Set G}
(hf : DifferentiableOn β f s)
(h0 : β x β s, f x β 0)
:
DifferentiableOn β (fun (y : G) => βf yβ) s
theorem
DifferentiableOn.dist
(π : Type u_1)
{E : Type u_2}
[RCLike π]
[NormedAddCommGroup E]
[InnerProductSpace π E]
[NormedSpace β E]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace β G]
{f g : G β E}
{s : Set G}
(hf : DifferentiableOn β f s)
(hg : DifferentiableOn β g s)
(hne : β x β s, f x β g x)
:
DifferentiableOn β (fun (y : G) => dist (f y) (g y)) s
Convenience aliases of PiLp
lemmas for EuclideanSpace
#
theorem
differentiableWithinAt_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{t : Set H}
{y : H}
:
DifferentiableWithinAt π f t y β β (i : ΞΉ), DifferentiableWithinAt π (fun (x : H) => f x i) t y
theorem
differentiableAt_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{y : H}
:
DifferentiableAt π f y β β (i : ΞΉ), DifferentiableAt π (fun (x : H) => f x i) y
theorem
differentiableOn_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{t : Set H}
:
DifferentiableOn π f t β β (i : ΞΉ), DifferentiableOn π (fun (x : H) => f x i) t
theorem
differentiable_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
:
Differentiable π f β β (i : ΞΉ), Differentiable π fun (x : H) => f x i
theorem
hasStrictFDerivAt_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{f' : H βL[π] EuclideanSpace π ΞΉ}
{y : H}
:
HasStrictFDerivAt f f' y β β (i : ΞΉ), HasStrictFDerivAt (fun (x : H) => f x i) ((PiLp.proj 2 (fun (x : ΞΉ) => π) i).comp f') y
theorem
hasFDerivWithinAt_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{f' : H βL[π] EuclideanSpace π ΞΉ}
{t : Set H}
{y : H}
:
HasFDerivWithinAt f f' t y β β (i : ΞΉ), HasFDerivWithinAt (fun (x : H) => f x i) ((PiLp.proj 2 (fun (x : ΞΉ) => π) i).comp f') t y
theorem
contDiffWithinAt_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{t : Set H}
{y : H}
{n : WithTop ββ}
:
ContDiffWithinAt π n f t y β β (i : ΞΉ), ContDiffWithinAt π n (fun (x : H) => f x i) t y
theorem
contDiffAt_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{y : H}
{n : WithTop ββ}
:
ContDiffAt π n f y β β (i : ΞΉ), ContDiffAt π n (fun (x : H) => f x i) y
theorem
contDiffOn_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{t : Set H}
{n : WithTop ββ}
:
ContDiffOn π n f t β β (i : ΞΉ), ContDiffOn π n (fun (x : H) => f x i) t
theorem
contDiff_euclidean
{π : Type u_1}
{ΞΉ : Type u_2}
{H : Type u_3}
[RCLike π]
[NormedAddCommGroup H]
[NormedSpace π H]
[Fintype ΞΉ]
{f : H β EuclideanSpace π ΞΉ}
{n : WithTop ββ}
:
theorem
PartialHomeomorph.contDiff_univUnitBall
{n : ββ}
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace β E]
:
theorem
PartialHomeomorph.contDiffOn_univUnitBall_symm
{n : ββ}
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace β E]
:
ContDiffOn β (βn) (βPartialHomeomorph.univUnitBall.symm) (Metric.ball 0 1)
theorem
Homeomorph.contDiff_unitBall
{n : ββ}
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace β E]
:
theorem
PartialHomeomorph.contDiff_unitBallBall
{n : ββ}
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace β E]
{c : E}
{r : β}
(hr : 0 < r)
:
ContDiff β βn β(PartialHomeomorph.unitBallBall c r hr)
theorem
PartialHomeomorph.contDiff_unitBallBall_symm
{n : ββ}
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace β E]
{c : E}
{r : β}
(hr : 0 < r)
:
ContDiff β βn β(PartialHomeomorph.unitBallBall c r hr).symm
theorem
PartialHomeomorph.contDiff_univBall
{n : ββ}
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace β E]
{c : E}
{r : β}
:
ContDiff β βn β(PartialHomeomorph.univBall c r)
theorem
PartialHomeomorph.contDiffOn_univBall_symm
{n : ββ}
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace β E]
{c : E}
{r : β}
:
ContDiffOn β (βn) (β(PartialHomeomorph.univBall c r).symm) (Metric.ball c r)