ResidualCorrectorExistence

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

The residual corrector w on the truncated window

The replacement draft's item 2 defines the residual corrector w by a Dirichlet problem on the truncated window V = (x+□_{n-2}) ∩ □_m and then uses two things about it: that it is harmonic (AffineSplitHarmonic.exists_affineSplit) and that it is bounded by the boundary data (BoundaryLaneMaxPrinciple).

The datum, honestly (disclosed)

HasBoundaryUpperBoundOn and MemH10 are stated in CoarseGraining's rigid convention: the H¹₀ witness must equal the given function as a total function on Vec d, not merely a.e. on V. The bound on the printed datum `h

• ℓ_h (AffineSplitLift.abs_sub_affineLift_volumeAverage_le) is available only *on the window*. exists_h1_clampbridges the two: it produces an `H¹(V)datum that is globally bounded byMand agrees with the original wherever the original is bounded byM` — in particular on all of the window, under the residual bound. This is a carrier adjustment, not a mathematical hypothesis: no bound is assumed anywhere it is not proved.

Main results

• exists_weaklyHarmonicOn_of_datum — the Dirichlet problem on any open bounded convex nonempty window, at the Laplacian.
• hasBoundaryUpperBoundOn_of_datum_le — the weak boundary bound from the datum.
• exists_h1_clamp — the globally clamped datum.
• exists_residualCorrector — the packaged corrector: harmonic, with the datum's trace, and two-sidedly bounded by M.
• exists_residualCorrector_truncatedWindow — the same on the boundary lane's own window (x+□_k) ∩ □_m.

What is not done here

The draft's split boundary data ("h - ℓ_h on ∂V ∩ ∂□_m and 0 on ∂V ∩ □_m") is replaced by the single datum h - ℓ_h on all of ∂V. This is a proof-route choice, not a statement change: the sup bound that item 2(ii) needs is ‖h-ℓ_h‖_{L^∞} on the whole window either way, so the corrector produced here carries exactly the constant the draft's does.

References

• CoarseGraining, PDE/DirichletRHS.lean, Sobolev/PotentialSolenoidalL2.lean, Sobolev/Truncation/{Basic,MatchedTrace}.lean.

1. The identity coefficient field

def Algsuperdiff.Section4.Provider.ExcessDecay.unitCoeffField (d : ℕ) : HCPolySupport.CoeffField d

The identity coefficient field, as CoarseGraining's constant field at scalarMatrix 1.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.unitCoeffField d = HCPolySupport.constantCoeffField (HCPolySupport.scalarMatrix 1)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.matVecMul_unitCoeffField {d : ℕ} (x v : HCPolySupport.Vec d) : HCPolySupport.matVecMul (unitCoeffField d x) v = v

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isEllipticFieldOn_unitCoeffField {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) : HCPolySupport.IsEllipticFieldOn 1 1 V (unitCoeffField d)

2. The Dirichlet problem on the window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_weaklyHarmonicOn_of_datum {d : ℕ} [NeZero d] {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hne : V.Nonempty) (Φ : HCPolySupport.H1Function V) : ∃ (w : HCPolySupport.H1Function V), Support.IsWeaklyHarmonicOn V w ∧ HCPolySupport.MemH10 V fun (y : HCPolySupport.Vec d) => w.toFun y - Φ.toFun y

The residual corrector exists.

On any open bounded convex nonempty window V and for any H¹(V) datum Φ there is a weakly harmonic w with w - Φ ∈ H¹₀(V): the draft's Dirichlet problem for the residual corrector.

3. The boundary bound from the datum

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasBoundaryUpperBoundOn_of_datum_le {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {w Φ : HCPolySupport.H1Function V} {M : ℝ} (hdiff : HCPolySupport.MemH10 V fun (y : HCPolySupport.Vec d) => w.toFun y - Φ.toFun y) (hΦ : ∀ (y : HCPolySupport.Vec d), Φ.toFun y ≤ M) : HasBoundaryUpperBoundOn V w M

4. The globally clamped datum

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_h1_clamp {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (Φ : HCPolySupport.H1Function V) {M : ℝ} (hM : 0 ≤ M) : ∃ (Ψ : HCPolySupport.H1Function V), (∀ (y : HCPolySupport.Vec d), Ψ.toFun y ≤ M) ∧ (∀ (y : HCPolySupport.Vec d), -M ≤ Ψ.toFun y) ∧ ∀ (y : HCPolySupport.Vec d), |Φ.toFun y| ≤ M → Ψ.toFun y = Φ.toFun y

The globally clamped datum. Every H¹(V) function has an H¹(V) clamp at level M, globally bounded by M and unchanged wherever the original already satisfies |Φ| ≤ M. This is the carrier bridge described in the module docstring, built from CoarseGraining's positive-part truncation applied to Φ and -Φ.

5. The packaged corrector

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_residualCorrector {d : ℕ} [NeZero d] {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hne : V.Nonempty) (Φ : HCPolySupport.H1Function V) {M : ℝ} (hupper : ∀ (y : HCPolySupport.Vec d), Φ.toFun y ≤ M) (hlower : ∀ (y : HCPolySupport.Vec d), -M ≤ Φ.toFun y) : ∃ (w : HCPolySupport.H1Function V), Support.IsWeaklyHarmonicOn V w ∧ (HCPolySupport.MemH10 V fun (y : HCPolySupport.Vec d) => w.toFun y - Φ.toFun y) ∧ HasBoundaryUpperBoundOn V w M ∧ HasBoundaryUpperBoundOn V (-w) M

The residual corrector, packaged.