ZeroTraceSupNorm

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

The supremum norm of a function vanishing on the boundary of a cube

A function on y + □_n that extends continuously to the closed cube and vanishes on its boundary is bounded by its own 1/2-Hölder seminorm:

  ‖w‖_{L^∞(y+□_n)} ≤ (3^n / 2)^{1/2} [w]_{C^{0,1/2}(y+□_n)} .

The proof is the one-line geometric argument. The ambient norm of Vec d = Fin d → ℝ is the supremum norm, so y + □_n is the ball of radius 3^n/2 around y; every point x of it lies on a radius whose endpoint z₀ is a boundary point at distance 3^n/2 - ‖x - y‖ ≤ 3^n/2, the segment from x to z₀ stays inside the cube, and the Hölder bound along that segment passes to the endpoint by continuity, where the value is zero.

Since (3^n/2)^{1/2} ≤ 3^{n/2}, the bound is also stated with the constant 3^{n/2} in which the localized estimates of Section 5 are written.

For a Sobolev function the boundary hypothesis is the zero-trace property, and no regularity beyond it is needed: Section5/Support/ZeroTraceBoundary.lean shows that a representative of an H¹₀ function takes arbitrarily small values arbitrarily close to the boundary, which is exactly what the geometric argument consumes at the endpoint of the radius.

References

• ABK26, the localized estimates of Section 5.1.

1. The cube of the supremum norm is a ball

theorem Algsuperdiff.Section5.Support.cubeSetAt_eq_ball {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : cubeSetAt y n = Metric.ball y (1 / 2 * 3 ^ n)

y + □_n is the ball of radius 3^n/2 around y, because the ambient norm of Vec d is the supremum norm.

theorem Algsuperdiff.Section5.Support.closure_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : closure (cubeSetAt y n) = Metric.closedBall y (1 / 2 * 3 ^ n)

theorem Algsuperdiff.Section5.Support.frontier_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : frontier (cubeSetAt y n) = Metric.sphere y (1 / 2 * 3 ^ n)

theorem Algsuperdiff.Section5.Support.mem_closure_cubeSetAt_iff {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} : x ∈ closure (cubeSetAt y n) ↔ ‖x - y‖ ≤ 1 / 2 * 3 ^ n

theorem Algsuperdiff.Section5.Support.mem_frontier_cubeSetAt_iff {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} : x ∈ frontier (cubeSetAt y n) ↔ ‖x - y‖ = 1 / 2 * 3 ^ n

theorem Algsuperdiff.Section5.Support.mem_cubeSetAt_iff_norm_sub_lt {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} : x ∈ cubeSetAt y n ↔ ‖x - y‖ < 1 / 2 * 3 ^ n

2. A radius through a point of the cube

3. The bound for a function vanishing on the boundary

4. A function vanishing outside the closed cube

theorem Algsuperdiff.Section5.Support.closure_cubeSetAt_subset_cubeSetAt_succ {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : closure (cubeSetAt y n) ⊆ cubeSetAt y (n + 1)

5. The zero-trace Sobolev function

theorem Algsuperdiff.Section5.Support.supNormOn_le_of_zeroTrace {d : ℕ} (hd : 0 < d) {y : HCPolySupport.Vec d} {n : ℤ} {v : HCPolySupport.H1Function (cubeSetAt y n)} (hw : ∃ (w : HCPolySupport.H10Function (cubeSetAt y n)), ∀ (x : HCPolySupport.Vec d), v.toFun x = w.toFun x) {vRep : HCPolySupport.Vec d → ℝ} (hrep : IsCubeRepresentative y n v vRep) : supNormOn (cubeSetAt y n) vRep ≤ ENNReal.ofReal ((1 / 2 * 3 ^ n) ^ (1 / 2)) * holderSeminormOn (cubeSetAt y n) (1 / 2) vRep

The continuous representative of a zero-trace Sobolev function is bounded on y + □_n by its own 1/2-Hölder seminorm, with the sharp constant (3^n/2)^{1/2}, the square root of the largest distance from a point of the cube to the boundary along a radius.

No regularity beyond membership in H¹₀ is assumed: the boundary values of the representative are read off from the translation estimate for the zero extension.

theorem Algsuperdiff.Section5.Support.supNormOn_le_rpow_mul_holderSeminormOn_of_zeroTrace {d : ℕ} (hd : 0 < d) {y : HCPolySupport.Vec d} {n : ℤ} {v : HCPolySupport.H1Function (cubeSetAt y n)} (hw : ∃ (w : HCPolySupport.H10Function (cubeSetAt y n)), ∀ (x : HCPolySupport.Vec d), v.toFun x = w.toFun x) {vRep : HCPolySupport.Vec d → ℝ} (hrep : IsCubeRepresentative y n v vRep) : supNormOn (cubeSetAt y n) vRep ≤ ENNReal.ofReal (Real.rpow 3 (↑n / 2)) * holderSeminormOn (cubeSetAt y n) (1 / 2) vRep

The same bound with the constant 3^{n/2} in which the localized estimates of Section 5 are written.