HarmonicReplaceDirichlet

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

The Laplace-Dirichlet solve with divergence-form right-hand side

The harmonic replacement of a function on a cube is obtained by subtracting the H^1_0 solution of a Dirichlet problem whose forcing is the whole right-hand side of the equation the function solves. The only elliptic solve the argument needs is therefore the one at the identity coefficient field:

  - Delta phi = div g  in  U ,   phi in H^1_0 (U) ,

in the weak form int_U <grad phi, grad psi> = int_U <g, grad psi> for every psi in H^1_0 (U).

CoarseGraining proves the general divergence-form Dirichlet solvability exists_isZeroTraceDirichletRhsWeakSolution_of_potentialZeroTraceClosureRealization conditionally on HasPotentialZeroTraceClosureRealization U, and discharges that condition on every bounded open convex domain (hasPotentialZeroTraceClosureRealization_of_isOpenBoundedConvexDomain). This module composes the two at the scalar coefficient field 1, where the flux matVecMul (scalarMatrix 1) v is v itself, and states the result in the gradient-pairing form the harmonic replacement consumes.

The a = 1 case is re-derived here directly from CoarseGraining; nothing from the manuscript-facing Provider/Corrector/DirichletClosure.lean (which is ABK-specific and restricted to triadic cubes) is used, so the domain class is the general one and the file stays portable.

Contents

• isEllipticFieldOn_one -- the constant identity coefficient field is elliptic with lam = Lam = 1 on every measurable set.
• exists_h10Function_integral_vecDot_grad_eq -- the solve: on a nonempty bounded open convex domain, every L^2 forcing field admits an H^1_0 potential whose Dirichlet pairing against every H^1_0 competitor reproduces the pairing of the forcing.

Portability

This file depends only on Mathlib, on CoarseGraining (Homogenization.*) and on the harmonic layer of this same directory. It mentions no object of the manuscript: no model, no cutoff, no shell, no corrector, no sigmaBar. It is intended to be portable into CoarseGraining by a single mechanical namespace rename.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.isEllipticFieldOn_one {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) : HCPolySupport.IsEllipticFieldOn 1 1 U fun (x : HCPolySupport.Vec d) => HCPolySupport.scalarMatrix 1

The constant identity coefficient field is elliptic with lam = Lam = 1 on every measurable set.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_h10Function_integral_vecDot_grad_eq {d : ℕ} [NeZero d] {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hne : U.Nonempty) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 U g) : ∃ (φ : HCPolySupport.H10Function U), ∀ (ψ : HCPolySupport.H10Function U), ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (φ.grad x) (ψ.grad x) = ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (g x) (ψ.grad x)

The Laplace-Dirichlet solve with divergence-form right-hand side.

On a nonempty bounded open convex domain U, every L^2 vector field g admits an H^1_0 (U) potential phi with

  int_U <grad phi, grad psi> = int_U <g, grad psi>   for every  psi in H^1_0 (U) .

This is CoarseGraining's conditional Dirichlet solvability at the scalar coefficient field 1, with the closure-realization hypothesis discharged by CoarseGraining's bounded open convex realization theorem.