Derivatives on WithLp

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)] {n : WithTop ℕ∞} {f : H → PiLp p E} {t : Set H} {y : H} : ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun (x : H) => (f x).ofLp i) t y

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)] {n : WithTop ℕ∞} {f : H → PiLp p E} {t : Set H} {y : H} (hf : ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun (x : H) => (f x).ofLp i) t y) : ContDiffWithinAt 𝕜 n f t y

theorem contDiffWithinAt_piLp_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)] {n : WithTop ℕ∞} {i : ι} {t : Set (PiLp p E)} {y : PiLp p E} : ContDiffWithinAt 𝕜 n (fun (f : PiLp p E) => f.ofLp 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)] {n : WithTop ℕ∞} {f : H → PiLp p E} {y : H} : ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun (x : H) => (f x).ofLp i) 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)] {n : WithTop ℕ∞} {f : H → PiLp p E} {y : H} (hf : ∀ (i : ι), ContDiffAt 𝕜 n (fun (x : H) => (f x).ofLp i) y) : ContDiffAt 𝕜 n f y

theorem contDiffAt_piLp_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)] {n : WithTop ℕ∞} {i : ι} {y : PiLp p E} : ContDiffAt 𝕜 n (fun (f : PiLp p E) => f.ofLp 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)] {n : WithTop ℕ∞} {f : H → PiLp p E} {t : Set H} : ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun (x : H) => (f x).ofLp i) t

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)] {n : WithTop ℕ∞} {f : H → PiLp p E} {t : Set H} (hf : ∀ (i : ι), ContDiffOn 𝕜 n (fun (x : H) => (f x).ofLp i) t) : ContDiffOn 𝕜 n f t

theorem contDiffOn_piLp_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)] {n : WithTop ℕ∞} {i : ι} {t : Set (PiLp p E)} : ContDiffOn 𝕜 n (fun (f : PiLp p E) => f.ofLp 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)] {n : WithTop ℕ∞} {f : H → PiLp p E} : ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun (x : H) => (f x).ofLp i

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)] {n : WithTop ℕ∞} {f : H → PiLp p E} (hf : ∀ (i : ι), ContDiff 𝕜 n fun (x : H) => (f x).ofLp i) : ContDiff 𝕜 n f

theorem contDiff_piLp_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)] {n : WithTop ℕ∞} {i : ι} : ContDiff 𝕜 n fun (f : PiLp p E) => f.ofLp i

theorem PiLp.contDiff_ofLp {𝕜 : 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)] {n : WithTop ℕ∞} : ContDiff 𝕜 n WithLp.ofLp

theorem PiLp.contDiff_toLp {𝕜 : 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)] {n : WithTop ℕ∞} : ContDiff 𝕜 n (WithLp.toLp p)

theorem WithLp.contDiff_ofLp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {n : WithTop ℕ∞} : ContDiff 𝕜 n ofLp

theorem WithLp.contDiff_toLp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)] {n : WithTop ℕ∞} : ContDiff 𝕜 n (toLp p)