BoundaryCaccioppoliDatum

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

The boundary regime of the coarse-grained Caccioppoli inequality with

l.coarse.grained.Caccioppoli.RHS is stated with a boundary datum h, and its right-hand side carries the extra leg t^{-3} Λ_t ‖∇h‖²_{H^{2t}(□_0)}. This module proves the other half of the printed lemma's own proof, the boundary reduction:

let v be the Dirichlet solution on the whole cube with the same force g and the same boundary datum h; then u - v has zero trace on all of ∂□_0 and solves the homogeneous equation, so the zero-data theorem applies to it, and the ∇h-leg is produced separately by the global energy estimate for ∇v.

Landed here: everything about u - v.

Main results

• This is what makes the boundary application legitimate at a patch that meets ∂□_m.
• memVectorL2_flux, isForcedEquation_sub — the flux pairing is integrable and the difference of two forced solutions with the same force solves the homogeneous equation.
• boundaryForcedCaccioppoliDatumOfDifference — CoarseGraining's datum, populated for u - v at zero force.
• exists_boundaryCaccioppoliEnergy_ofDifference — CoarseGraining's coarse Caccioppoli applied to it: the core energy of u - v is bounded by the pure L² term, the force leg having vanished.

What is not done here

Three things separate this from the printed boundary display on x + □_n:

1. the triangle inequality ‖σ^{1/2}∇u‖ ≤ ‖σ^{1/2}∇(u-v)‖ + ‖σ^{1/2}∇v‖ on the core (a quadratic-form Minkowski step);
2. the volume-ratio conversion of the global energy norm of v to the core (a d-only constant, needing a lower bound on |caccioppoliCoreSet Q x|);

None of the three is asserted anywhere in this file.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS, (the reduction), and its boundary application.
• CoarseGraining, CoarseCaccioppoli/Theory.lean, Energy/Theory.lean, PublicInternalBridges/CoeffField.lean, Sobolev/PotentialSolenoidalL2.lean.

2. The flux pairing and the homogeneous difference equation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memVectorL2_flux {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) : HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch02.cubeDomain Q).carrier fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x) (u.grad x)

The flux a ∇u of an H¹ function is square integrable on the cube: the coefficient field has an everywhere-elliptic representative (CoarseGraining's publicCoeffField) agreeing with it almost everywhere.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integrableOn_flux_pairing {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (φ : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x) (u.grad x)) (φ.grad x)) (HCPolySupport.Book.Ch02.cubeDomain Q).carrier MeasureTheory.volume

The tested flux pairing is integrable.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isForcedEquation_sub {d : ℕ} {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily 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) : HCPolySupport.Book.Ch03.IsForcedEquation Q a (u - v) fun (x : HCPolySupport.Vec d) => 0

The difference of two forced solutions with the same force is a solution of the homogeneous equation. This is the first step of the printed proof of l.coarse.grained.Caccioppoli.RHS.

3. The zero force is admissible

theorem Algsuperdiff.Section4.Provider.ExcessDecay.forceBesovRegularity_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) : HCPolySupport.Book.Ch03.ForceBesovRegularity Q s fun (x : HCPolySupport.Vec d) => 0

The zero force has the H^s regularity CoarseGraining's Caccioppoli theorem asks of its right-hand side.