theorem
differentiableWithinAt_piLp
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup H]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 H]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
{f : H → PiLp p E}
{t : Set H}
{y : H}
:
DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun (x : H) => f x i) t y
theorem
differentiableAt_piLp
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup H]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 H]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
{f : H → PiLp p E}
{y : H}
:
DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun (x : H) => f x i) y
theorem
differentiableOn_piLp
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup H]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 H]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
{f : H → PiLp p E}
{t : Set H}
:
DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun (x : H) => f x i) t
theorem
differentiable_piLp
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup H]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 H]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
{f : H → PiLp p E}
:
Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun (x : H) => f x i
theorem
hasStrictFDerivAt_piLp
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup H]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 H]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
{f : H → PiLp p E}
{f' : H →L[𝕜] PiLp p E}
{y : H}
:
HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) => f x i) ((PiLp.proj p E i).comp f') y
theorem
hasFDerivWithinAt_piLp
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
{H : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup H]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 H]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
{f : H → PiLp p E}
{f' : H →L[𝕜] PiLp p E}
{t : Set H}
{y : H}
:
HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) => f x i) ((PiLp.proj p E i).comp f') t y