Documentation

LeanPool.EllipticPDE.Regularity.CutoffDatum

Datum of the induction step #

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 step 3 produces an equation for the cut-off derivative whose datum is a fixed list of shapes. Each is the middle cutoff of the tower, or one of its first two partial derivatives, against a coefficient of the operator or one of its derivatives, against a derivative of the solution of order at most two.

This file builds that datum as a single L²(Ω) class, with its order-k family, its bound and its pairing. Nothing here knows how the list arose: the expansion of the bilinear form and the differentiated equation both live in EllipticPdes.Regularity.HigherInterior, and what they need of the datum is exactly the three conclusions below.

The constant is quantified before the solution, the datum and the direction of differentiation. The shapes that differentiate a coefficient in the direction the equation is differentiated depend on that direction, so their constants are collected over it.

Main declarations #

source
noncomputable def EllipticPdes.Regularity.cutoffDatumPairing {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {k : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 2)) (hbc : IsWkInftyLower Op (k + 1)) {N : Set (EuclideanSpace ℝ (Fin (n + 1)))} (ξ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) (ℓ : Fin (n + 1)) (uN Df : Sobolev.L2D N) (HuN : HasIteratedWeakDerivOn N (k + 2) uN) (v : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) :
ℝ

Pairing of the twelve pieces in the differentiated, cut-off datum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem EllipticPdes.Regularity.exists_cutoffDatum {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω N : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hNm : MeasurableSet N) (hNΩ : N ⊆ Ω) {k : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 2)) (hbc : IsWkInftyLower Op (k + 1)) {ξ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hξ : Sobolev.IsTestFn N ξ) :
    ∃ (K : ℝ), 0 ≤ K ∧ ∀ (ℓ : Fin (n + 1)) (uN Df : Sobolev.L2D N) (HuN : HasIteratedWeakDerivOn N (k + 2) uN) (HDf : HasIteratedWeakDerivOn N k Df) (B : ℝ), IteratedL2Bound HuN B → IteratedL2Bound HDf B → ∃ (F : Sobolev.L2D Ω) (HF : HasIteratedWeakDerivOn Ω k F), IteratedL2Bound HF (K * B) ∧ ∀ (v : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), ContDiff ℝ (↑⊤) v → HasCompactSupport v → ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑F x * v x = cutoffDatumPairing Op hA hbc ξ ℓ uN Df HuN v

    Datum of the induction step. For a cutoff ξ supported in the collar N ⊆ Ω, there is a constant such that every family of derivatives of the solution on N bounded by B, and every derivative of the datum bounded by B, produce an L²(Ω) class with k weak derivatives bounded by K·B and pairing against a test function as the twelve shapes.

    The two shapes with the zeroth-order coefficient against the differentiated solution cancel between the differentiated equation and the zeroth-order block, and are absent. The two with the transport coefficient do not, because the equation names one order of differentiation and the block the other, and only the symmetry of the mixed second derivatives identifies them.