Smooth cutoff tower for the interior H² estimate

The interior second-derivative estimate (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8) localises the difference-quotient method with a nested family of smooth cutoffs: an innermost cutoff ζ equal to 1 on the region of interest V, a middle cutoff ξ equal to 1 on the support of ζ, and an outermost cutoff θ equal to 1 on the support of ξ, all three compactly supported inside the ambient domain Ω. The outermost support has a positive margin δ: every point of tsupport θ stays inside Ω after a coordinate shift h eₖ of size |h| < δ, which is exactly what lets the discrete difference quotient act inside Ω without losing mass.

This file provides:

• exists_isTestFn_one_nhdsSet_of_isCompact: the underlying smooth Urysohn-type cutoff lemma: for K compact inside an open U, a test function on U valued in [0,1] and equal to 1 on a neighbourhood of K. This specialises the classical smooth-partition-of-unity construction (Mathlib.Geometry.Manifold.PartitionOfUnity) to the trivial self-chart manifold structure that EuclideanSpace ℝ (Fin d) has as a finite-dimensional normed space, bridged back to plain ContDiff via contMDiff_iff_contDiff.
• exists_margin_of_isCompact_subset_isOpen: the positive-margin fact for a compact-in-open pair, from IsCompact.exists_cthickening_subset_open.
• CutoffTower: the bundle of the three nested cutoffs and the margin.
• cutoffTowerOfIsCompactSubsetIsOpen: existence of a CutoffTower for every compact V inside an open Ω, built by three applications of the Urysohn-type cutoff lemma followed by one application of the margin lemma.

Urysohn-type smooth cutoff on a compact-in-open pair

theorem EllipticPdes.Regularity.exists_isTestFn_one_nhdsSet_of_isCompact {d : ℕ} {K U : Set (EuclideanSpace ℝ (Fin d))} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (ζ : EuclideanSpace ℝ (Fin d) → ℝ), Sobolev.IsTestFn U ζ ∧ (∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet K, ζ x = 1) ∧ ∀ (x : EuclideanSpace ℝ (Fin d)), ζ x ∈ Set.Icc 0 1

Smooth Urysohn cutoff. For K compact contained in an open U, a test function on U (EllipticPdes.Sobolev.IsTestFn), valued in [0,1], equal to 1 on a neighbourhood of K. This is the smooth cutoff-function device used throughout interior regularity theory (Evans, Partial Differential Equations (2nd ed.), §6.3.1), obtained here from the manifold smooth-partition-of-unity Urysohn lemma specialised to the self-chart manifold structure EuclideanSpace ℝ (Fin d) has as a finite-dimensional normed space.

Positive shift margin on a compact-in-open pair

theorem EllipticPdes.Regularity.exists_margin_of_isCompact_subset_isOpen {d : ℕ} {K Ω : Set (EuclideanSpace ℝ (Fin d))} (hK : IsCompact K) (hΩ : IsOpen Ω) (hKΩ : K ⊆ Ω) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (k : Fin d) (h : ℝ), |h| < δ → ∀ x ∈ K, x + hshift k h ∈ Ω

Positive margin. For K compact inside an open Ω, there is δ > 0 such that every point of K stays inside Ω after any coordinate shift h eₖ with |h| < δ. This is the finite-margin fact that lets the interior difference-quotient method translate a cutoff's support without leaving the domain (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8).

Nested cutoff tower

structure EllipticPdes.Regularity.CutoffTower {d : ℕ} (Ω V : Set (EuclideanSpace ℝ (Fin d))) : Type

Nested cutoff tower. Three test functions on Ω: ζ equal to 1 on the base compact set V, ξ equal to 1 on the support of ζ, θ equal to 1 on the support of ξ, together with a positive coordinate-shift margin valid on the support of θ. This is exactly the tower ζ, ξ, θ nested in that support-inclusion order, localising the difference-quotient method of the interior H² estimate (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8).

• ζ : EuclideanSpace ℝ (Fin d) → ℝ

  The innermost cutoff, equal to 1 on V.

• ξ : EuclideanSpace ℝ (Fin d) → ℝ

  The middle cutoff, equal to 1 on tsupport ζ.

• θ : EuclideanSpace ℝ (Fin d) → ℝ

  The outermost cutoff, equal to 1 on tsupport ξ.

• hζ : Sobolev.IsTestFn Ω self.ζ

  ζ is a test function on Ω.

• hξ : Sobolev.IsTestFn Ω self.ξ

  ξ is a test function on Ω.

• hθ : Sobolev.IsTestFn Ω self.θ

  θ is a test function on Ω.

• hζ_Icc (x : EuclideanSpace ℝ (Fin d)) : self.ζ x ∈ Set.Icc 0 1

  ζ is valued in [0,1].

• hξ_Icc (x : EuclideanSpace ℝ (Fin d)) : self.ξ x ∈ Set.Icc 0 1

  ξ is valued in [0,1].

• hθ_Icc (x : EuclideanSpace ℝ (Fin d)) : self.θ x ∈ Set.Icc 0 1

  θ is valued in [0,1].

• hζ_one : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet V, self.ζ x = 1

  ζ ≡ 1 on a neighbourhood of V.

• hξ_one : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet (tsupport self.ζ), self.ξ x = 1

  ξ ≡ 1 on a neighbourhood of tsupport ζ.

• hθ_one : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet (tsupport self.ξ), self.θ x = 1

  θ ≡ 1 on a neighbourhood of tsupport ξ.

• margin : ℝ

  The positive coordinate-shift margin on tsupport θ.

• hmargin_pos : 0 < self.margin

  The margin is positive.

• hmargin (k : Fin d) (h : ℝ) : |h| < self.margin → ∀ x ∈ tsupport self.θ, x + hshift k h ∈ Ω

  Below the margin, every point of tsupport θ stays inside Ω after a coordinate shift.

theorem EllipticPdes.Regularity.CutoffTower.zeta_eqOn_one {d : ℕ} {Ω V : Set (EuclideanSpace ℝ (Fin d))} (T : CutoffTower Ω V) : Set.EqOn T.ζ 1 V

The innermost cutoff is equal to 1 at every point of V, rather than on a neighbourhood of it.

theorem EllipticPdes.Regularity.CutoffTower.xi_eqOn_one {d : ℕ} {Ω V : Set (EuclideanSpace ℝ (Fin d))} (T : CutoffTower Ω V) : Set.EqOn T.ξ 1 (tsupport T.ζ)

The middle cutoff is equal to 1 at every point of tsupport ζ.

theorem EllipticPdes.Regularity.CutoffTower.theta_eqOn_one {d : ℕ} {Ω V : Set (EuclideanSpace ℝ (Fin d))} (T : CutoffTower Ω V) : Set.EqOn T.θ 1 (tsupport T.ξ)

The outermost cutoff is equal to 1 at every point of tsupport ξ.

noncomputable def EllipticPdes.Regularity.cutoffTowerOfIsCompactSubsetIsOpen {d : ℕ} {Ω V : Set (EuclideanSpace ℝ (Fin d))} (hV : IsCompact V) (hΩ : IsOpen Ω) (hVΩ : V ⊆ Ω) : CutoffTower Ω V

Existence of the cutoff tower. For any compact V inside an open Ω, a cutoff tower based at V exists: three applications of exists_isTestFn_one_nhdsSet_of_isCompact build ζ, ξ, θ in turn (each new cutoff's compact set is the topological support of the previous one, which stays inside Ω), and exists_margin_of_isCompact_subset_isOpen supplies the final margin on tsupport θ.

Equations

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