A one-sided cutoff along one coordinate

The extension by reflection is proved by testing strictly inside the half space and letting the excluded slab shrink. The cutoff that excludes it is a function of the j-th coordinate alone: slabCut j ε vanishes for xⱼ ≤ ε and is 1 for xⱼ ≥ 2ε, so a test function multiplied by it is supported in the open half space.

Two properties are what the limit needs. The partial derivatives along the interface vanish identically, so those directions leave no boundary term. The remaining one is bounded by C/ε and supported in the slab, which is what the odd part of the reflection cancels against.

Main declarations

• EllipticPdes.Extension.slabCut: the cutoff.
• EllipticPdes.Extension.slabCut_eq_zero, EllipticPdes.Extension.slabCut_eq_one: its values on the slab and beyond it.
• EllipticPdes.Extension.partialD_slabCut_of_ne: it is constant along the interface.
• EllipticPdes.Extension.norm_partialD_slabCut_le: the C/ε bound.

noncomputable def EllipticPdes.Extension.stepProfile : ℝ → ℝ

The one-sided profile: 0 for t ≤ 1, 1 for t ≥ 2, smooth, with values in [0, 1].

Equations

• EllipticPdes.Extension.stepProfile t = (t - 1).smoothTransition

theorem EllipticPdes.Extension.contDiff_stepProfile : ContDiff ℝ (↑⊤) stepProfile

theorem EllipticPdes.Extension.stepProfile_eq_zero {t : ℝ} (ht : t ≤ 1) : stepProfile t = 0

theorem EllipticPdes.Extension.stepProfile_eq_one {t : ℝ} (ht : 2 ≤ t) : stepProfile t = 1

theorem EllipticPdes.Extension.stepProfile_nonneg (t : ℝ) : 0 ≤ stepProfile t

theorem EllipticPdes.Extension.stepProfile_le_one (t : ℝ) : stepProfile t ≤ 1

theorem EllipticPdes.Extension.deriv_stepProfile_eq_zero_of_lt {t : ℝ} (ht : t < 1) : deriv stepProfile t = 0

The profile is constant below the slab, so its derivative vanishes there.

theorem EllipticPdes.Extension.deriv_stepProfile_eq_zero_of_gt {t : ℝ} (ht : 2 < t) : deriv stepProfile t = 0

The profile is constant above the slab, so its derivative vanishes there.

theorem EllipticPdes.Extension.exists_bound_deriv_stepProfile : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), |deriv stepProfile t| ≤ C

The profile is constant off [1, 2], so its derivative is continuous with compact support and therefore bounded.

The cutoff on the space

noncomputable def EllipticPdes.Extension.slabCut {d : ℕ} (j : Fin d) (ε : ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

Cutoff excluding the slab xⱼ ≤ ε. It depends on the j-th coordinate alone.

Equations

• EllipticPdes.Extension.slabCut j ε x = EllipticPdes.Extension.stepProfile (x.ofLp j / ε)

theorem EllipticPdes.Extension.contDiff_slabCut {d : ℕ} (j : Fin d) (ε : ℝ) : ContDiff ℝ (↑⊤) (slabCut j ε)

theorem EllipticPdes.Extension.slabCut_nonneg {d : ℕ} (j : Fin d) (ε : ℝ) (x : EuclideanSpace ℝ (Fin d)) : 0 ≤ slabCut j ε x

theorem EllipticPdes.Extension.slabCut_le_one {d : ℕ} (j : Fin d) (ε : ℝ) (x : EuclideanSpace ℝ (Fin d)) : slabCut j ε x ≤ 1

theorem EllipticPdes.Extension.slabCut_eq_zero {d : ℕ} {j : Fin d} {ε : ℝ} (hε : 0 < ε) {x : EuclideanSpace ℝ (Fin d)} (hx : x.ofLp j ≤ ε) : slabCut j ε x = 0

On the excluded slab the cutoff vanishes.

theorem EllipticPdes.Extension.slabCut_eq_one {d : ℕ} {j : Fin d} {ε : ℝ} (hε : 0 < ε) {x : EuclideanSpace ℝ (Fin d)} (hx : 2 * ε ≤ x.ofLp j) : slabCut j ε x = 1

Beyond the slab the cutoff is 1.

theorem EllipticPdes.Extension.partialD_slabCut {d : ℕ} {j : Fin d} {ε : ℝ} (_hε : 0 < ε) (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (slabCut j ε) x = deriv stepProfile (x.ofLp j / ε) * ((if j = k then 1 else 0) / ε)

The derivative of the cutoff, in every direction.

theorem EllipticPdes.Extension.partialD_slabCut_of_ne {d : ℕ} {j : Fin d} {ε : ℝ} (hε : 0 < ε) {k : Fin d} (hk : k ≠ j) (x : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (slabCut j ε) x = 0

Constancy of the cutoff along the interface.

theorem EllipticPdes.Extension.norm_partialD_slabCut_le {d : ℕ} {j : Fin d} {ε : ℝ} (hε : 0 < ε) {C : ℝ} (hC : ∀ (t : ℝ), |deriv stepProfile t| ≤ C) (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) : |Sobolev.partialD k (slabCut j ε) x| ≤ C / ε

Bound C/ε on the remaining partial derivative.

theorem EllipticPdes.Extension.partialD_slabCut_eq_zero_of_gt {d : ℕ} {j : Fin d} {ε : ℝ} (hε : 0 < ε) (k : Fin d) {x : EuclideanSpace ℝ (Fin d)} (hx : 2 * ε < x.ofLp j) : Sobolev.partialD k (slabCut j ε) x = 0

Support of the cutoff's derivative in the slab.

theorem EllipticPdes.Extension.tsupport_mul_slabCut_subset {d : ℕ} {j : Fin d} {ε : ℝ} (hε : 0 < ε) (ψ : EuclideanSpace ℝ (Fin d) → ℝ) : (tsupport fun (x : EuclideanSpace ℝ (Fin d)) => slabCut j ε x * ψ x) ⊆ {x : EuclideanSpace ℝ (Fin d) | 0 < x.ofLp j}

Vanishing of the cutoff off the open half space, so a test function multiplied by it is supported where the hypothesis of a weak gradient applies.