BoundaryAssemblyDirichlet

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

The rough-field Dirichlet solution with boundary datum h

This module removes that input: it constructs v, at the rough coefficient family a itself (not a constant background), from CoarseGraining's zero-trace Dirichlet well-posedness.

  ρ ∈ H¹₀(□_m)  solves  −∇·a∇ρ = ∇·(g − a∇h) ,      v := h + ρ .

Then −∇·a∇v = ∇·g weakly and v − h = ρ ∈ H¹₀(□_m) on the nose, which is exactly CoarseGraining's DirichletForcedCubeSolution with boundaryData = h.

The coefficient bridge

CoarseGraining's public weak formulation IsForcedEquation tests against (a.coeffOn Q).toCoeffField, while its Dirichlet existence theorem needs the everywhere-elliptic representative publicCoeffField Q a. The two agree a.e. on the cube (publicCoeffField_ae_eq), and integral_flux_eq_publicCoeffField below is the only place that fact is used.

Main results

• memVectorL2_roughDirichletCorrectorForce — the shifted force is L².
• exists_zeroTraceDirichletCorrector_rough — CoarseGraining's existence at the rough field on the open cube.
• memH10_sub_of_exact_zeroTrace — two solutions with the same datum and exact witnesses have a difference in H¹₀, which discharges the zero-trace hypothesis of the boundary Caccioppoli display.

What is not done here

No estimate of any kind: the energy of the solution constructed here is bounded by CoarseGraining's energyConsequencesRHSTheory, consumed in BoundaryAssemblyEnergy. Uniqueness of v is not claimed (it is not needed: every statement downstream is existential in v).

References

• ABK26, `l.coarse.grained.Caccioppoli.
• CoarseGraining/Dirichlet.lean, Book/Ch03/Definitions.lean (DirichletForcedCubeSolution), Book/Ch03/Theorems/PublicInternalBridges/CoeffField.lean`.

1. The coefficient bridge

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integral_flux_eq_publicCoeffField {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) : ∫ (x : HCPolySupport.Vec d) in (HCPolySupport.Book.Ch02.cubeDomain Q).carrier, HCPolySupport.vecDot (HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x) (u.grad x)) (φ.grad x) = ∫ (x : HCPolySupport.Vec d) in (HCPolySupport.Book.Ch02.cubeDomain Q).carrier, HCPolySupport.vecDot (HCPolySupport.matVecMul (HCPolySupport.Book.Ch03.publicCoeffField Q a x) (u.grad x)) (φ.grad x)

The tested flux pairing may be computed with CoarseGraining's everywhere-elliptic representative publicCoeffField Q a instead of the public CoeffOn field: the two agree almost everywhere on the cube.

2. The shifted force

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.roughDirichletCorrectorForce {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The force of the zero-trace problem solved by v − h. The printed force g minus the datum's own flux a∇h.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.roughDirichletCorrectorForce Q a h g x = g x - HCPolySupport.matVecMul (HCPolySupport.Book.Ch03.publicCoeffField Q a x) (h.grad x)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memVectorL2_roughDirichletCorrectorForce {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) (roughDirichletCorrectorForce Q a h g)

3. The zero-trace corrector at the rough field

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_zeroTraceDirichletCorrector_rough {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) : ∃ (rho : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (HCPolySupport.Book.Ch03.publicCoeffField Q a) (HCPolySupport.openCubeSet Q) rho (roughDirichletCorrectorForce Q a h g)

CoarseGraining's Dirichlet existence theorem at the rough field. Nothing in it is special to a constant background: it asks only for an elliptic field, and publicCoeffField Q a is one on the open cube.

4. The Dirichlet solution with boundary datum h

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_dirichletForcedCubeSolution_boundaryData {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) : ∃ (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution Q a g), v.boundaryData = h ∧ ∃ (rho : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)), ∀ (y : HCPolySupport.Vec d), rho.toFun y = v.toH1.toFun y - h.toFun y

The comparison solution of the printed boundary reduction.

For every boundary datum h ∈ H¹(□_m) and every square-integrable force g there is a Dirichlet forced solution on the cube whose boundary datum is exactly h.