ZeroTraceBoundary

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The boundary values of a zero-trace function on a cube

A function of H¹₀(y + □_n) has no pointwise boundary values, but a representative that is continuous up to the boundary does, and they vanish. This module proves that, with no regularity hypothesis whatsoever beyond membership in H¹₀ and the existence of the representative.

The mechanism is the translation estimate for the zero extension. Write w for the extension of w : H¹₀(y + □_n) by zero, an H¹ function of the whole space whose gradient is the zero extension of the gradient of w, and fix a coordinate direction e_i in which the boundary point x₀ sits on a face of the cube. For a step t the L² norm of the difference quotient (w(·) − w(· − t e_i))/t is at most the L² norm of ∂_i w, a quantity independent of t. If the representative had modulus at least ε on (y + □_n) ∩ B_ρ(x₀), then that difference quotient would have modulus at least ε/t on an explicit box of measure of order t · ρ^{d−1} just outside the face: the shifted point lies in the cube near x₀, where the modulus is at least ε, and the point itself lies outside the cube, where the extension vanishes. The two statements give ε² ρ^{d−1} ≲ t, which fails for small t.

At an edge or a corner of the cube the same box works: only one coordinate is moved, and the remaining coordinates are confined to intervals pushed into the cube by the fixed factor 1 − θ, which is what the box below records.

References

• ABK26, the localized estimates of Section 5.1.

1. The cube and its boundary in coordinates

theorem Algsuperdiff.Section5.Support.mem_cubeSetAt_iff_abs_coord {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} : x ∈ cubeSetAt y n ↔ ∀ (j : Fin d), |x j - y j| < 1 / 2 * 3 ^ n

Membership in y + □_n written with absolute values.

theorem Algsuperdiff.Section5.Support.abs_coord_le_of_mem_frontier_cubeSetAt {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x₀ : HCPolySupport.Vec d} (hx₀ : x₀ ∈ frontier (cubeSetAt y n)) (j : Fin d) : |x₀ j - y j| ≤ 1 / 2 * 3 ^ n

Every coordinate of a boundary point of y + □_n is within the half-width of the corresponding coordinate of the centre.

theorem Algsuperdiff.Section5.Support.exists_abs_coord_eq_of_mem_frontier_cubeSetAt {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x₀ : HCPolySupport.Vec d} (hx₀ : x₀ ∈ frontier (cubeSetAt y n)) : ∃ (i : Fin d), |x₀ i - y i| = 1 / 2 * 3 ^ n

A boundary point of y + □_n sits on a face: some coordinate attains the half-width exactly.

2. The box just outside a face

3. Arbitrarily small values arbitrarily close to the boundary

theorem Algsuperdiff.Section5.Support.exists_mem_cubeSetAt_abs_lt_of_mem_frontier {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (w : HCPolySupport.H10Function (cubeSetAt y n)) {v : HCPolySupport.Vec d → ℝ} (hv : v =ᵐ[MeasureTheory.volume.restrict (cubeSetAt y n)] w.toFun) {x₀ : HCPolySupport.Vec d} (hx₀ : x₀ ∈ frontier (cubeSetAt y n)) {rho eps : ℝ} (hrho : 0 < rho) (heps : 0 < eps) : ∃ x ∈ cubeSetAt y n, ‖x - x₀‖ < rho ∧ |v x| < eps

Arbitrarily close to a boundary point of y + □_n, and inside the cube, a representative of an H¹₀ function takes arbitrarily small values.