theorem
contDiffWithinAt_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}
{n : ℕ∞}
:
ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun (x : H) => f x i) t y
theorem
contDiffAt_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}
{n : ℕ∞}
:
ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun (x : H) => f x i) y
theorem
contDiffOn_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}
{n : ℕ∞}
:
ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun (x : H) => f x i) t
theorem
contDiff_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}
{n : ℕ∞}
: