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
theorem
PiLp.hasStrictFDerivAt_equiv
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
(f : PiLp p E)
:
HasStrictFDerivAt (⇑(WithLp.equiv p ((i : ι) → E i))) (↑(PiLp.continuousLinearEquiv p 𝕜 E)) f
theorem
PiLp.hasStrictFDerivAt_equiv_symm
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
(f : PiLp p E)
:
HasStrictFDerivAt (⇑(WithLp.equiv p ((i : ι) → E i)).symm) (↑(PiLp.continuousLinearEquiv p 𝕜 E).symm) f
theorem
PiLp.hasStrictFDerivAt_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
(f : PiLp p E)
(i : ι)
:
HasStrictFDerivAt (fun (f : PiLp p E) => f i) (PiLp.proj p E i) f
theorem
PiLp.hasFDerivAt_equiv
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
(f : PiLp p E)
:
HasFDerivAt (⇑(WithLp.equiv p ((i : ι) → E i))) (↑(PiLp.continuousLinearEquiv p 𝕜 E)) f
theorem
PiLp.hasFDerivAt_equiv_symm
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
(f : PiLp p E)
:
HasFDerivAt (⇑(WithLp.equiv p ((i : ι) → E i)).symm) (↑(PiLp.continuousLinearEquiv p 𝕜 E).symm) f
theorem
PiLp.hasFDerivAt_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : ι → Type u_3}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
(f : PiLp p E)
(i : ι)
:
HasFDerivAt (fun (f : PiLp p E) => f i) (PiLp.proj p E i) f