35 Partial differential equations

TheoremEuler's theorem on homogeneous functions #

Mathlib records this with 3 declarations.

HasFDerivAt.apply_self_eq_smul_of_eventuallyEq: A local, vector-valued version of Euler's theorem on homogeneous functions.

If f (t • x) = w t • f x for t in a neighborhood of 1, then the derivative of f at x, applied to x, is w' • f x, where w' is the derivative of w at 1.

HasFDerivAt.apply_self_eq_smul_of_eventuallyEq.{u_1, u_2, u_3} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {x : E} {L : E →L[𝕜] F} {w : 𝕜 → 𝕜} {w' : 𝕜}
  (hf : HasFDerivAt f L x) (hw : HasDerivAt w w' 1)
  (hhom : (fun t => f (t • x)) =ᶠ[nhds 1] fun t => w t • f x) : L x = w' • f x

HasFDerivAt.apply_self_eq_smul_of_homogeneous: A vector-valued version of Euler's theorem for a homogeneous function.

If f (t • y) = w t • f y for all scalars t and points y, then the derivative of f at x, applied to x, is w' • f x, where w' is the derivative of w at 1.

HasFDerivAt.apply_self_eq_smul_of_homogeneous.{u_1, u_2, u_3} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {x : E} {L : E →L[𝕜] F} {w : 𝕜 → 𝕜} {w' : 𝕜}
  (hf : HasFDerivAt f L x) (hw : HasDerivAt w w' 1)
  (hhom : ∀ (t : 𝕜) (y : E), f (t • y) = w t • f y) : L x = w' • f x

HasFDerivAt.apply_self_eq_nsmul_of_homogeneous: A vector-valued version of Euler's theorem for a homogeneous function of natural degree.

If f (t • y) = t ^ k • f y for all scalars t and points y, then the derivative of f at x, applied to x, is k • f x.

HasFDerivAt.apply_self_eq_nsmul_of_homogeneous.{u_1, u_2, u_3} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {x : E} {L : E →L[𝕜] F} {k : ℕ}
  (hf : HasFDerivAt f L x) (hhom : ∀ (t : 𝕜) (y : E), f (t • y) = t ^ k • f y) : L x = k • f x

The converse stated in the English Wikipedia article is not yet formalized.

Sources

MathlibHasFDerivAt.apply_self_eq_smul_of_eventuallyEq · HasFDerivAt.apply_self_eq_smul_of_homogeneous · HasFDerivAt.apply_self_eq_nsmul_of_homogeneous

Uses 6

Statement usesDerivative at a point · Differentiable function between normed vector spaces · Finite set · Normed vector space over a normed field

Proof usesAssociative algebra over a commutative ring · Topology on a normed vector space

Lax–Milgram theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

35 Partial differential equations

TheoremEuler's theorem on homogeneous functions#

Sources

TheoremEuler's theorem on homogeneous functions #