BoundaryOuterCaccioppoli

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

The boundary Caccioppoli display at the localized boundary datum

This module re-proves the same display at the hypothesis the covering route can actually discharge — CoarseGraining's own LocalizedZeroTraceFunctionOn through the Dirichlet patch, which is precisely the field BoundaryForcedCaccioppoliDatum.zeroTraceOnBoundaryPatch and no more.

The discharge itself is the point:

  u - v  =  (u - h)  -  (v - h)
             ↑ H¹₀(□_m), localized on c+□_k through the patch
                          ↑ H¹₀(c+□_k), localized through anything

so localizedZeroTraceFunctionOn_sub closes it, and BoundaryDatumTransport moves the whole thing into □_k's own frame.

Main results

• boundaryForcedCaccioppoliDatumOfLocalizedDifference — CoarseGraining's datum populated by a difference with only a localized zero trace.
• exists_boundaryCaccioppoliEnergy_ofLocalizedDifference — the printed e.cgC.boundary.applied at that hypothesis.
• exists_boundaryCaccioppoliEnergy_withLocalizedBoundaryDatum — with both legs (the [g]_{B^r} force leg and the ‖∇h‖_{B^r} boundary leg), at the localized hypothesis.
• localizedZeroTraceFunctionOn_wellPlacedDifference — the discharge, in the covering cube's own frame.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS.
• CoarseGraining, Book/Ch03/Theorems/CoarseCaccioppoli/Theory.lean, Book/Ch03/Theorems/Energy/Theory.lean, Sobolev/H1/LocalizedZeroTrace.lean.

1. The datum at the localized hypothesis

def Algsuperdiff.Section4.Provider.ExcessDecay.boundaryForcedCaccioppoliDatumOfLocalizedDifference {d : ℕ} {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} (x : HCPolySupport.Vec d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {u v : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier} (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) (hv : HCPolySupport.Book.Ch03.IsForcedEquation Q a v g) (hdiff : HCPolySupport.Book.Ch01.LocalizedZeroTraceFunctionOn (HCPolySupport.Book.Ch02.cubeDomain Q).carrier (HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 1)) fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) : HCPolySupport.Book.Ch03.BoundaryForcedCaccioppoliDatum Q a x fun (x : HCPolySupport.Vec d) => 0

CoarseGraining's boundary Caccioppoli datum, populated by a difference with only a localized zero trace.

On the covering cube only the localized statement is available, and only the localized statement is needed: it is the field.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.boundaryForcedCaccioppoliDatumOfLocalizedDifference x hu hv hdiff = { toH1 := u - v, weakSolution := ⋯, zeroTraceOnBoundaryPatch := ⋯ }

2. The printed boundary display at the localized hypothesis

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundaryCaccioppoliEnergy_ofLocalizedDifference (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {s t : ℝ} {x : HCPolySupport.Vec d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (u v : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier), HCPolySupport.Book.Ch03.IsForcedEquation Q a u g → HCPolySupport.Book.Ch03.IsForcedEquation Q a v g → (HCPolySupport.Book.Ch01.LocalizedZeroTraceFunctionOn (HCPolySupport.Book.Ch02.cubeDomain Q).carrier (HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 1)) fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) → 0 < s → s < 1 → 0 < t → t < 1 / 2 → s + t < 1 → x ∈ HCPolySupport.openCubeSet Q → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x) (a.coeffOn Q) (u - v) ≤ HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C Q a s t * (HCPolySupport.Book.Ch02.lambdaS Q t a * Real.rpow 3 (-2 * ↑Q.scale) * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y)

e.cgC.boundary.applied at the localized boundary datum.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundaryCaccioppoliEnergy_withLocalizedBoundaryDatum (d : ℕ) [NeZero d] : ∃ (C₁ : ℝ) (C₂ : ℝ), 0 < C₁ ∧ 0 < C₂ ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {s t r : ℝ} {x : HCPolySupport.Vec d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution Q a g), HCPolySupport.Book.Ch03.IsForcedEquation Q a u g → (HCPolySupport.Book.Ch01.LocalizedZeroTraceFunctionOn (HCPolySupport.Book.Ch02.cubeDomain Q).carrier (HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 1)) fun (y : HCPolySupport.Vec d) => u.toFun y - v.toH1.toFun y) → 0 < s → s < 1 → 0 < t → t < 1 / 2 → s + t < 1 → 0 < r → r < 1 → HCPolySupport.Book.Ch03.ForceBesovRegularity Q r g → HCPolySupport.Book.Ch03.ForceBesovRegularity Q r (HCPolySupport.Book.Ch03.dirichletBoundaryGradientField v) → x ∈ HCPolySupport.openCubeSet Q → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x) (a.coeffOn Q) u ≤ 2 * (HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C₁ Q a s t * (HCPolySupport.Book.Ch02.lambdaS Q t a * Real.rpow 3 (-2 * ↑Q.scale) * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => u.toFun y - v.toH1.toFun y)) + 2 * (18 ^ d * HCPolySupport.Book.Ch03.dirichletEnergyWithRHSRHS C₂ Q a r g v ^ 2)

** at the localized boundary datum: the boundary-regime coarse Caccioppoli estimate with both ∇h legs.**

3. The discharge, in the covering cube's own frame

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_wellPlacedDifference {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (hkm : k ≤ m) (rho : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (sigma : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d k))) {U V : HCPolySupport.Vec d → ℝ} (hUV : ∀ (y : HCPolySupport.Vec d), U y - V y = rho.toFun (y + wellPlacedCentre x m k) - sigma.toFun y) : HCPolySupport.Book.Ch01.LocalizedZeroTraceFunctionOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) (HCPolySupport.Book.Ch03.openCubeAtScale (x - wellPlacedCentre x m k) (k - 1)) fun (y : HCPolySupport.Vec d) => U y - V y

The localized zero trace of u - v on the well-placed covering cube.

The anchor's own H¹₀(□_m) witness ρ (its boundary condition u = h) and the comparison solution's own H¹₀(□_k) witness σ (v = h on ∂□_k) combine: u - v = ρ(·+c) - σ in the covering cube's frame, and the localized zero trace is closed under subtraction.