BoundaryCoveringTrace

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

The boundary datum on the covering cube

The last hypothesis CoarseGraining's boundary coarse Caccioppoli inequality asks of its datum, once the covering cube of BoundaryCoveringGeometry is in place, is the localized zero trace through the Dirichlet patch:

  LocalizedZeroTraceFunctionOn (c + □_k) (openCubeAtScale x (k-1)) (u - v) .

Here the ambient domain is □_m but the Caccioppoli domain is the smaller covering cube, so the H¹₀ witness has to descend. It does, and for exactly the reason the covering was designed: a cutoff supported in the patch multiplies the H¹₀(□_m) approximants into functions supported in patch ∩ □_m, and that set is inside the covering cube.

Main results

• h10RestrictOfApproxSupport — an H¹₀(Ω) function whose approximants are all supported in an open W ⊆ Ω is an H¹₀(W) function, with the same value, gradient and approximating sequence.
• localizedZeroTraceFunctionOn_of_memH10_of_inter_subset — the descent: a global zero trace on Ω gives the localized zero trace on W through every window V with V ∩ Ω ⊆ W.
• localizedZeroTraceFunctionOn_wellPlacedCube — the instance at the covering cube, with the geometric hypothesis discharged by BoundaryCoveringGeometry.

What is not done here

This is stated in the untranslated frame, with the covering cube as a translated set. Feeding it to CoarseGraining's theorem, which is stated at a TriadicCube, requires the A4 translation transport of the datum (sample translation); that step belongs to the development's TranslationTransport* lane and is not taken here. Nothing in this module asserts the Caccioppoli estimate.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS; boundary application.
• CoarseGraining, Sobolev/H1/LocalizedZeroTrace.lean, Sobolev/H1/Algebra/H10Function.lean, Sobolev/H1/BasicLemmas.lean.

1. The H¹₀ descent

def Algsuperdiff.Section4.Provider.ExcessDecay.h10RestrictOfApproxSupport {d : ℕ} {Ω W : Set (HCPolySupport.Vec d)} (hWopen : IsOpen W) (hWΩ : W ⊆ Ω) (u : HCPolySupport.H10Function Ω) (hsupp : ∀ (n : ℕ), tsupport (u.approx n) ⊆ W) : HCPolySupport.H10Function W

H¹₀ descends along the support of its approximants.

If every smooth compactly supported approximant of u ∈ H¹₀(Ω) is supported in the open subset W ⊆ Ω, then u is an H¹₀(W) function: the same value, the same weak gradient, the same approximating sequence. Only the two L² convergences have to be re-read, and they are inherited because eLpNorm is monotone in the measure.

Equations

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

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10RestrictOfApproxSupport_toFun {d : ℕ} {Ω W : Set (HCPolySupport.Vec d)} (hWopen : IsOpen W) (hWΩ : W ⊆ Ω) (u : HCPolySupport.H10Function Ω) (hsupp : ∀ (n : ℕ), tsupport (u.approx n) ⊆ W) : (h10RestrictOfApproxSupport hWopen hWΩ u hsupp).toFun = u.toFun

2. The localized zero trace on a subdomain

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_of_memH10_of_inter_subset {d : ℕ} {Ω W V : Set (HCPolySupport.Vec d)} (hWopen : IsOpen W) (hWΩ : W ⊆ Ω) (hVW : V ∩ Ω ⊆ W) (u : HCPolySupport.H10Function Ω) : HCPolySupport.LocalizedZeroTraceFunctionOn W V u.toFun

The boundary datum descends to the covering set.

A function with a global zero trace on Ω has the localized zero trace on any open W ⊆ Ω through any window V with V ∩ Ω ⊆ W.

3. The instance at the well-placed covering cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_image_add_openCubeSet_originCube {d : ℕ} (z : HCPolySupport.Vec d) (k : ℤ) : IsOpen ((fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k))

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_wellPlacedCube {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (hkm : k ≤ m) (u : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : HCPolySupport.LocalizedZeroTraceFunctionOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) (HCPolySupport.Book.Ch03.openCubeAtScale x (k - 1)) u.toFun

The Caccioppoli boundary datum on the covering cube.

For k ≤ m, a function with a global zero trace on □_m has the localized zero trace on the well-placed covering cube c + □_k through the Dirichlet patch openCubeAtScale x (k-1) — the exact hypothesis of CoarseGraining's BoundaryForcedCaccioppoliDatum at an outer cube of scale k.

The geometric input is BoundaryCoveringGeometry: the cube stays in □_m, and it covers the truncated patch (x+□_{k-1}) ∩ □_m.