Higher-order datum of the cutoff reduction

The cutoff reduction of Local/Reduction.lean hands η U an equation whose datum pairs f, U₀ and the gradient coordinates of U against bounded weights supported in tsupport η. The higher-order induction of Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 applies the H₀¹ theorem at order k to η U, and so asks the datum for k weak derivatives with a bound.

Every term of the datum is a cutoff, a W^{k,∞} coefficient and a coordinate of U, which is the shape exists_datum_of_pieces assembles. The coordinates of U are only asked for k weak derivatives on the support of the cutoff, which is what the induction has available one order down; the datum f is asked for them on Ω. The derivative of the principal coefficient is the first member of its W^{k+1,∞} family, through IsWkInftyCoeff.coeffWeakGrad, so the pairing reads off reduction_testFn with no classical derivative anywhere.

Main declarations

• setIntegral_cutoff_restrict_eq: a piece on the support of the cutoff as an integral on Ω.
• exists_reductionDatum: the datum, its family, its bound and its pairing.
• exists_collarFamily_of_weakDerivOn: exists_collarFamily with a weak derivative on the outer set in place of one on the whole space.

theorem EllipticPdes.Regularity.setIntegral_cutoff_restrict_eq {d : ℕ} {Ω N : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : tsupport χ ⊆ N) (c v : EuclideanSpace ℝ (Fin d) → ℝ) (g : Sobolev.L2D Ω) : ∫ (x : EuclideanSpace ℝ (Fin d)) in N, χ x * (c x * ↑↑(restrictL2 ((extendL2 hΩm) g)) x) * v x = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, c x * ↑↑g x * (χ x * v x)

Piece on the support of the cutoff as an integral on Ω. For χ supported in N, pairing the restriction of g to N against χ c v on N is pairing g against c χ v on Ω.

theorem EllipticPdes.Regularity.exists_reductionDatum {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω N : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hNm : MeasurableSet N) (hNΩ : N ⊆ Ω) {k : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 1)) (hbc : IsWkInftyLower Op k) {η : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hη : Sobolev.IsTestFn N η) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (U : Sobolev.H1amb Ω) (f : Sobolev.L2D Ω) (HU : (j : Fin (n + 2)) → HasIteratedWeakDerivOn N k (restrictL2 ((extendL2 hΩm) (U.ofLp j)))) (Hf : HasIteratedWeakDerivOn Ω k f) (B : ℝ), (∀ (j : Fin (n + 2)), IteratedL2Bound (HU j) B) → IteratedL2Bound Hf 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 = (((((∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑f x * (η x * v x)) - ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, Op.a x i j * ↑↑(U.ofLp i.succ) x * (Sobolev.partialD j η x * v x)) - ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, hA.coeffWeakGrad.da j i j x * ↑↑(U.ofLp 0) x * (Sobolev.partialD i η x * v x)) - ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, Op.a x i j * ↑↑(U.ofLp j.succ) x * (Sobolev.partialD i η x * v x)) - ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, Op.a x i j * ↑↑(U.ofLp 0) x * (Sobolev.partialD j (Sobolev.partialD i η) x * v x)) + ∑ i : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, Op.b x i * ↑↑(U.ofLp 0) x * (Sobolev.partialD i η x * v x)

Datum of the cutoff reduction at order k. For a cutoff η supported in N ⊆ Ω, with W^{k+1,∞} principal and W^{k,∞} transport coefficients, there is a constant K such that every U whose coordinates have k weak derivatives on N, and every datum f with k weak derivatives on Ω, all bounded by B, give an L²(Ω) class with k weak derivatives bounded by K B pairing against a test function as the datum of reduction_testFn.

theorem EllipticPdes.Regularity.exists_collarFamily_of_weakDerivOn {d : ℕ} {Ω W N : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (hNm : MeasurableSet N) (hNW : N ⊆ W) {θ : EuclideanSpace ℝ (Fin d) → ℝ} (hθW : Sobolev.IsTestFn W θ) (hθN : Set.EqOn θ 1 N) {g : Sobolev.L2D Ω} {Dg : Fin d → Sobolev.L2D Ω} (hDgW : ∀ (i : Fin d), HasWeakDerivOn W i (restrictL2 ((extendL2 hΩm) g)) (restrictL2 ((extendL2 hΩm) (Dg i)))) {m : ℕ} {C : ℝ} (HuW : HasIteratedWeakDerivOn W (m + 1) (restrictL2 ((extendL2 hΩm) g))) (hHuW : IteratedL2Bound HuW C) : ∃ (HuN : HasIteratedWeakDerivOn N (m + 1) (restrictL2 ((extendL2 hΩm) g))), IteratedL2Bound HuN C ∧ ∀ (i : Fin d), HuN.D [i] = restrictL2 ((extendL2 hΩm) (Dg i))

Inductive family moved to the collar from a weak derivative on the outer set. The statement of exists_collarFamily, with the whole-space weak derivative of g replaced by one on W. A solution with no boundary condition has its gradient as a weak derivative on Ω and on every subset, and never on the whole space after extension by zero.