Documentation

Mathlib.Analysis.Calculus.FDeriv.WithLp

Derivatives on WithLp #

source
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
source
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
source
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
source
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
source
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
source
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
source
theorem PiLp.hasStrictFDerivAt_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)] (f : PiLp p E) :
HasStrictFDerivAt WithLp.ofLp (↑(continuousLinearEquiv p 𝕜 E)) f
source
@[deprecated PiLp.hasStrictFDerivAt_ofLp (since := "2025-05-07")]
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 : (i : ι) → E i) :
HasStrictFDerivAt (⇑(WithLp.equiv p ((i : ι) → E i))) (↑(continuousLinearEquiv p 𝕜 E)) f
source
theorem PiLp.hasStrictFDerivAt_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)] (f : (i : ι) → E i) :
HasStrictFDerivAt (WithLp.toLp p) (↑(continuousLinearEquiv p 𝕜 E).symm) f
source
@[deprecated PiLp.hasStrictFDerivAt_toLp (since := "2025-05-07")]
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 : (i : ι) → E i) :
HasStrictFDerivAt (⇑(WithLp.equiv p ((i : ι) → E i)).symm) (↑(continuousLinearEquiv p 𝕜 E).symm) f
source
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) (proj p E i) f
source
theorem PiLp.hasFDerivAt_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)] (f : PiLp p E) :
HasFDerivAt WithLp.ofLp (↑(continuousLinearEquiv p 𝕜 E)) f
source
@[deprecated PiLp.hasFDerivAt_ofLp (since := "2025-05-07")]
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))) (↑(continuousLinearEquiv p 𝕜 E)) f
source
theorem PiLp.hasFDerivAt_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)] (f : (i : ι) → E i) :
HasFDerivAt (WithLp.toLp p) (↑(continuousLinearEquiv p 𝕜 E).symm) f
source
@[deprecated PiLp.hasFDerivAt_toLp (since := "2025-05-07")]
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 : (i : ι) → E i) :
HasFDerivAt (⇑(WithLp.equiv p ((i : ι) → E i)).symm) (↑(continuousLinearEquiv p 𝕜 E).symm) f
source
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) (proj p E i) f