Documentation

LeanPool.EllipticPDE.Regularity.CoeffBridge

Classical Cᵏ coefficients satisfy Guo's W^{k,∞} hypothesis #

EllipticPdes.Regularity.IsCkCoeff states the coefficient hypothesis of Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2: every entry is Cᵏ with a uniform bound on each iteratedFDeriv. EllipticPdes.Regularity.IsWkInftyCoeff states the weaker hypothesis of Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65): weak derivatives up to order k, essentially bounded. This file connects them, so that a theorem proved under Guo's hypothesis applies to smooth coefficients with no further work.

The bridge needs two facts and nothing else. A classical partial derivative of a C¹ function is a weak partial derivative, which is integration by parts against a compactly supported test function. A classical iterated partial derivative is a value of iteratedFDeriv on unit vectors, so the operator-norm bound of IsCkCoeff transfers to it pointwise, and a pointwise bound is in particular an essential bound.

Iterated classical partial derivative #

iterPartial f α applies partialD once per entry of α, outermost first, so that iterPartial f (l :: α) = ∂_l (iterPartial f α). This is the cons convention of IsWkInftyCoeff.D, which is what makes iterPartial a legal choice of D.

Main declarations #

Unit vectors along a list of directions #

source
def EllipticPdes.Regularity.dirVec {d : ℕ} (α : List (Fin d)) :
Fin α.length → EuclideanSpace ℝ (Fin d)

The tuple of coordinate unit vectors named by a list of directions, in the order the list gives them. This is the argument iteratedFDeriv is evaluated at to produce an iterated partial derivative.

Equations
Instances For
    source
    @[simp]
    theorem EllipticPdes.Regularity.dirVec_cons_zero {d : ℕ} (l : Fin d) (α : List (Fin d)) :
    dirVec (l :: α) 0 = EuclideanSpace.single l 1
    source
    @[simp]
    theorem EllipticPdes.Regularity.dirVec_cons_tail {d : ℕ} (l : Fin d) (α : List (Fin d)) :
    Fin.tail (dirVec (l :: α)) = dirVec α
    source
    theorem EllipticPdes.Regularity.norm_dirVec {d : ℕ} (α : List (Fin d)) (i : Fin α.length) :
    ‖dirVec α i‖ = 1

    Every entry of dirVec is a unit vector, so a multilinear bound evaluated on it loses nothing.

    Iterated classical partial derivative #

    source
    def EllipticPdes.Regularity.iterPartial {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) :
    List (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ

    The iterated classical partial derivative along a list of directions, outermost first: iterPartial f (l :: α) = ∂_l (iterPartial f α). The cons convention matches IsWkInftyCoeff.D, whose D_step differentiates the head.

    Equations
    Instances For
      source
      @[simp]
      theorem EllipticPdes.Regularity.iterPartial_nil {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) :
      iterPartial f [] = f
      source
      @[simp]
      theorem EllipticPdes.Regularity.iterPartial_cons {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) (l : Fin d) (α : List (Fin d)) :
      iterPartial f (l :: α) = Sobolev.partialD l (iterPartial f α)
      source
      theorem EllipticPdes.Regularity.contDiff_iterPartial {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (α : List (Fin d)) {n : ℕ} :
      ContDiff ℝ (↑↑(n + α.length)) f → ContDiff ℝ (↑↑n) (iterPartial f α)

      Each differentiation spends one order of smoothness: f ∈ C^{n + |α|} gives iterPartial f α ∈ Cⁿ.

      source
      theorem EllipticPdes.Regularity.iterPartial_eq_iteratedFDeriv {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (α : List (Fin d)) {n : ℕ} :
      α.length ≤ n → ContDiff ℝ (↑↑n) f → ∀ (x : EuclideanSpace ℝ (Fin d)), iterPartial f α x = (iteratedFDeriv ℝ α.length f x) (dirVec α)

      Iterated partial derivative as a value of iteratedFDeriv. Applying partialD once per entry of α produces iteratedFDeriv ℝ |α| f x evaluated on the unit vectors α names. The proof peels the head with iteratedFDeriv_succ_apply_left, which differentiates the |α|-th derivative once more, and commutes that derivative past the evaluation at a fixed tuple, which is a continuous linear map.

      source
      theorem EllipticPdes.Regularity.abs_iterPartial_le {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (α : List (Fin d)) {n : ℕ} (hα : α.length ≤ n) (hf : ContDiff ℝ (↑↑n) f) (x : EuclideanSpace ℝ (Fin d)) :
      |iterPartial f α x| ≤ ‖iteratedFDeriv ℝ α.length f x‖

      The iterated partial derivative is bounded by the operator norm of the corresponding iteratedFDeriv, because it is that multilinear map evaluated on unit vectors.

      Classical derivative as a weak derivative #

      source
      theorem EllipticPdes.Regularity.hasWeakPartial_partialD {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : ContDiff ℝ (↑↑1) f) (l : Fin d) :
      HasWeakPartial l f (Sobolev.partialD l f)

      Integration by parts for a C¹ function against a test function. The classical partial derivative of a continuously differentiable function is its weak partial derivative. No decay is asked of f, because the test function has compact support and puts every integrand into L¹.

      Bridge #

      source
      noncomputable def EllipticPdes.Regularity.IsCkCoeff.toIsWkInftyCoeff {d : ℕ} {A : Sobolev.EllipticCoeff d} {k : ℕ} (hA : IsCkCoeff A k) :
      IsWkInftyCoeff A k

      Cᵏ coefficient bundle as a W^{k,∞} bundle. The classical iterated partial derivatives serve as the weak derivative family, each step is integration by parts, and the pointwise iteratedFDeriv bound of IsCkCoeff is in particular an essential bound.

      Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) is therefore no weaker than Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 as far as the coefficients go, and a result proved under IsWkInftyCoeff applies to smooth coefficients through this map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For