FreshShellSumWeakBridge

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

The two weak formulations of e.def.w and the potential/solenoidal pair

ABK26, e.def.w and e.corrector.limit.pde.

The manuscript writes the fresh-shell correctors as the solutions of -Delta w = div f on cu_K, once with zero trace and once with the mean-zero Neumann gauge. The formalization records this in two different but equivalent shapes:

• the weak-solution shape used by the recurrence consumers (Provider/Diffusivity/ApproximateRecurrence/**, Provider/Diffusivity/Corrector/FreshShellExistence.lean): IsZeroTraceDirichletRhsWeakSolution 1 U w (-f) and IsMeanZeroNeumannRhsWeakSolution 1 U w (-f);
• the Helmholtz shape used by the corrector-limit endpoints (Provider/Corrector/CorrectorLimitNode.lean, Provider/Corrector/FreshShellCorrectorEnergy.lean): IsPotentialZeroTraceOn U (grad w) together with IsSolenoidalOn U (grad w + f), respectively IsPotentialOn U (grad w) together with IsSolenoidalZeroNormalTraceOn U (grad w + f).

This module proves the two shapes equivalent, in both directions, at an arbitrary carrier U. Nothing here is specific to a cube, to a shell law or to a model: the content is the first-variation identity read twice.

Relation to the existing existential forms

Provider/Corrector/CorrectorLimitNonVacuity.lean already proves the existential statements exists_isPotentialZeroTraceOn_and_isSolenoidalOn_openCubeSet_of_continuous and exists_isPotentialOn_and_isSolenoidalZeroNormalTraceOn_openCubeSet_of_continuous: at a continuous forcing on a triadic cube some Helmholtz pair exists, obtained by solving the cube problem and reading its solution in the Helmholtz shape. Those statements do not help a consumer that already has the two correctors w_D, w_N -- which is exactly the situation of ApproximateRecurrence/LocalizationRecurrenceMesh.lean, whose _of_freshShellCorrectors form produces them. This module exports the statement for a given solution, in both directions, at an arbitrary carrier and without any continuity hypothesis.

Why the equivalence is not a triviality on the Neumann side

IsMeanZeroNeumannRhsWeakSolution tests against H1MeanZeroFunction U only, while IsSolenoidalZeroNormalTraceOn tests against all of H1Function U. The two agree because subtracting its own average from a test function does not change its gradient (H1Function.grad_subAverage) and proves it in the mean-zero gauge (H1Function.meanZeroOn_subAverage); the enlargement of the test class therefore costs nothing. This step needs U to carry a finite volume measure, which is why the Neumann statements alone carry the [IsFiniteMeasure (volumeMeasureOn U)] instance.

Main results

• isSolenoidalOn_grad_add_of_isZeroTraceDirichletRhsWeakSolution_one, isSolenoidalZeroNormalTraceOn_grad_add_of_isMeanZeroNeumannRhsWeakSolution_one -- weak formulation ⟹ solenoidality of the corrected field, in the zero-trace Dirichlet gauge and in the mean-zero Neumann gauge respectively.

The identity coefficient field

The Dirichlet shape

theorem Algsuperdiff.Section3.Provider.Corrector.isSolenoidalOn_grad_add_of_isZeroTraceDirichletRhsWeakSolution_one {d : ℕ} {U : Set (HCPolySupport.Vec d)} {w : HCPolySupport.H10Function U} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 U f) (hw : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) U w fun (x : HCPolySupport.Vec d) => -f x) : HCPolySupport.IsSolenoidalOn U fun (x : HCPolySupport.Vec d) => w.grad x + f x

Weak zero-trace formulation ⟹ solenoidality of the corrected field.

If w solves -div (grad w) = div (-f) in the zero-trace weak sense, then grad w + f is solenoidal against zero-trace test gradients: this is the same first-variation identity with the two sides collected.

The Neumann shape

theorem Algsuperdiff.Section3.Provider.Corrector.isSolenoidalZeroNormalTraceOn_grad_add_of_isMeanZeroNeumannRhsWeakSolution_one {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] {w : HCPolySupport.H1MeanZeroFunction U} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 U f) (hw : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) U w fun (x : HCPolySupport.Vec d) => -f x) : HCPolySupport.IsSolenoidalZeroNormalTraceOn U fun (x : HCPolySupport.Vec d) => w.toH1Function.grad x + f x

Weak mean-zero Neumann formulation ⟹ solenoidality with zero normal trace.

The enlargement of the test class from the mean-zero gauge to all of H¹(U) is free: subtracting the average of a test function changes neither its gradient nor the two integrals.