HomLiftEndpoint

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

Theorem B, §4.5, Step 3c: the L^∞ endpoint of the Hölder lifting

What this module proves

Step 3 of Theorem B asserts

  3^{-m} ‖u - v‖_{L^∞(□_m)} ≤ C 3^{-ms} ‖∇u - ∇v‖_{W_hat^{-s,∞}(□_m)}

for the Dirichlet pair u, v of the manuscript, whose difference satisfies `u

• v ∈ H^1_0(□_m)`.

Once the Hölder lifting of HomLiftTelescope has produced [w]_{C^{0,1-s}(□_m)} ≤ K, the L^∞ endpoint is elementary: w vanishes on ∂□_m, every point of □_m is within sup-distance 3^m of a boundary point, and therefore

  3^{-m} |w(x)| ≤ 3^{-m} K (3^m)^{1-s} = K 3^{-ms}   for every x ∈ □_m,

with constant exactly 1. This is linfty_of_holder_of_boundary_zero_cube.

The boundary carrier

The zero boundary value is carried literally: w vanishes on cubeFaceSet Q = closedCubeSet Q \ openCubeSet Q. This is the pointwise form of u - v ∈ H^1_0(□_m) for the continuous representative the Hölder bound produces, and it is stated as an explicit hypothesis rather than derived from an H^1_0 witness: the trace theorem that turns u - v ∈ H^1_0 into pointwise vanishing on ∂□_m is not in the tree.

Main results

• closedCubeSet, cubeFaceSet — the closed realization of a triadic cube and its topological boundary.
• norm_sub_le_cubeScaleFactor — the sup-diameter of a triadic cube is its side length 3^{scale} (the hdiam hypothesis of the lifting).
• linfty_of_holder_of_boundary_zero_cube — the endpoint display, at constant 1.
• ae_linfty_of_holder_of_boundary_zero_cube — the same, in the ∀ᵐ x form the frozen statement literally uses.

References

• ABK26, Theorem B Step 3.
• ABK26 (the W^{-s,∞} ↔ Hölder remark, "for functions vanishing on the boundary").

1. The closed cube and its faces

def Algsuperdiff.Section4.Provider.Homogenization.closedCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : Set (HCPolySupport.Vec d)

The closed realization of a triadic cube: openCubeSet with both inequalities relaxed. CoarseGraining carries the open and half-open realizations only; the closed one is what the boundary argument needs.

Equations

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

def Algsuperdiff.Section4.Provider.Homogenization.cubeFaceSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : Set (HCPolySupport.Vec d)

The face set of a triadic cube: the closed realization minus the open one.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.cubeFaceSet Q = Algsuperdiff.Section4.Provider.Homogenization.closedCubeSet Q \ HCPolySupport.openCubeSet Q

theorem Algsuperdiff.Section4.Provider.Homogenization.openCubeSet_subset_closedCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.openCubeSet Q ⊆ closedCubeSet Q

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeScaleFactor_pos {d : ℕ} (Q : HCPolySupport.TriadicCube d) : 0 < HCPolySupport.cubeScaleFactor Q

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_scale_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) : 3 ^ ↑Q.scale = HCPolySupport.cubeScaleFactor Q

The side length as a real power of 3 at the cube's scale.

2. The sup-diameter of a triadic cube

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_sub_le_cubeScaleFactor {d : ℕ} (Q : HCPolySupport.TriadicCube d) (x : HCPolySupport.Vec d) : x ∈ closedCubeSet Q → ∀ y ∈ closedCubeSet Q, ‖x - y‖ ≤ 3 ^ ↑Q.scale

The diameter estimate. In the ambient sup norm of Vec d, two points of the closed triadic cube Q are at distance at most the side length 3^{Q.scale}. This is the hdiam hypothesis of the Hölder lifting.

3. The boundary point

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_face_point {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet Q) : ∃ y ∈ cubeFaceSet Q, ‖x - y‖ ≤ 3 ^ ↑Q.scale

Every point of the open cube has a face point of the same cube at sup-distance at most the side length: move one coordinate to the upper face and leave the others alone.

4. The L^∞ endpoint

theorem Algsuperdiff.Section4.Provider.Homogenization.linfty_of_holder_of_boundary_zero_cube {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {w : HCPolySupport.Vec d → ℝ} {s K : ℝ} (hs1 : s < 1) (hK : 0 ≤ K) (hHol : Support.HolderSeminormBoundOn (closedCubeSet Q) (1 - s) K w) (hzero : ∀ y ∈ cubeFaceSet Q, w y = 0) (x : HCPolySupport.Vec d) : x ∈ HCPolySupport.openCubeSet Q → 3 ^ (-↑Q.scale) * |w x| ≤ K * 3 ^ (-↑Q.scale * s)

The L^∞ endpoint of the lifting.

If w obeys the Hölder bound [w]_{C^{0,1-s}} ≤ K on the closed cube and vanishes on the cube's faces, then

  3^{-scale} |w(x)| ≤ K · 3^{-scale·s}   for every x in the open cube.

The constant is exactly 1: the volume-normalized L^∞ gauge on the left and the Hölder seminorm on the right differ by exactly the factor (3^{scale})^{1-s} supplied by the cube's diameter.

5. The composition with the lifting

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_linfty_of_holder_of_boundary_zero_cube {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {w : HCPolySupport.Vec d → ℝ} {s K : ℝ} (hs1 : s < 1) (hK : 0 ≤ K) (hHol : Support.HolderSeminormBoundOn (closedCubeSet Q) (1 - s) K w) (hzero : ∀ y ∈ cubeFaceSet Q, w y = 0) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet Q), 3 ^ (-↑Q.scale) * |w x| ≤ K * 3 ^ (-↑Q.scale * s)

The ∀ᵐ x form used by the frozen root's conclusion (C3): the pointwise bound on the open cube upgrades to an almost-everywhere bound against the restricted volume measure.