BoundaryPoincareWindow #

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

The boundary-Poincaré opener: the covering cube inside the anchor window #

The general clause's right-hand-side windows are the enlarged ones, W' = (z+□_{n+3}) ∩ □_m rather than W = (z+□_{n+2}) ∩ □_m, precisely so that the boundary covering cube c + □_{n+2}, c = wellPlacedCentre x m (n+2), fits inside the window whose norms the anchor prices. This module proves that fit and the two transports it immediately supplies — the geometric half of the funded unit.

image_add_wellPlacedCentre_subset_anchorWindow — the fit: c + □_{n+2} ⊆ W'. It combines the two halves of CoveringSlotObstruction (the covering cube is inside z + □_{n+3}) and BoundaryCoveringGeometry (it is inside □_m).
volume_anchorWindow_le_coveringCube — the covering ratio |W'| ≤ 9^d |c+□_{n+2}| (the true ratio is 3^d; the perfect square is taken so that the L² constant is the integer power 3^d).
eLpNorm_coveringCube_le_anchorWindow — the L² transport: a normalized L² norm over the covering cube is at most 3^d times the one over the anchor's own window. This is the step that will move the boundary Caccioppoli's left-hand side into the frozen statement's carrier.
localizedZeroTraceFunctionOn_anchorWindow — the zero-trace localization onto W': a global H¹₀(□_m) datum has the localized zero trace on W' through the window z + □_{n+3}, because (z+□_{n+3}) ∩ □_m is W'.

What is not done here #

No Poincaré inequality is proved. The trace-measure lower bound, CoarseGraining's coarsePoincare and the Stampacchia machinery are the analytic half and are untouched; nothing below asserts any estimate on u - v, and nothing below is an instance, or a fraction, of any source node.

The fit proved here is a fit of windows, not of events.

References #

ABK26, l.harmonic.approximation.good.scales; the boundary application of l.coarse.grained.Caccioppoli.

1. The fit #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_wellPlacedCentre_subset_anchorWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) :

(fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The boundary covering cube sits inside the anchor's window.

This is what the window enlargement buys: with the printed n+2 window the covering cube provably does not fit (CoveringSlotObstruction), with the frozen n+3 window it always does.