InteriorAssemblyLhs

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

The interior clause's left-hand side, identified with the constructed

harmonic replacement

Steps (v) and (vi) of the interior-clause assembly: the frozen theorem quantifies over the harmonic function v and the H¹₀ witness w with v = u − w; every proved estimate is proved for the constructed replacement. This module closes the gap, in the anchor's own carriers:

  ‖u − v‖_{L²(x+□_n)}  =  ‖u − v⋆‖_{L²(□_n)}   at   v⋆ = harmonicReplacement σ u_tilde,

u_tilde = u(· + x) being the solution read in the child's own frame.

The three transported facts

• isWeaklyHarmonicOn_untranslate — weak harmonicity is translation covariant (the H¹₀ test functions correspond bijectively; the change of variables is measure preserving).
• isConstantCoeffForcedEquation_zero_of_isWeaklyHarmonicOn — −Δv = 0 and −∇·(σ Id)∇v = 0 are the same condition: the comparator is a positive scalar, and it factors out of the weak identity. This is where the frozen statement's Laplacian harmonicity (Support.IsWeaklyHarmonicOn) meets the development's comparator harmonicity (Ch03.IsConstantCoeffForcedEquation).
• H10Function.untranslate / H1Function.untranslate (CoarseGraining) — the carriers.

References

• ABK26, l.harmonic.approximation.good.scales; e.harmonic.approx.v.def.

1. Weak harmonicity untranslates

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_untranslate {d : ℕ} {U : Set (HCPolySupport.Vec d)} (z : HCPolySupport.Vec d) {v : HCPolySupport.H1Function (HCPolySupport.translateSet z U)} (h : Support.IsWeaklyHarmonicOn (HCPolySupport.translateSet z U) v) : Support.IsWeaklyHarmonicOn U (HCPolySupport.H1Function.untranslate z v)

Weak harmonicity in the back-translated frame.

If ∫_{U+z} ∇v · ∇φ = 0 for every φ ∈ H¹₀(U+z), then the same holds on U for v(· + z). Exact: no constant, no hypothesis beyond the statement.

2. Laplace harmonicity is comparator harmonicity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isConstantCoeffForcedEquation_zero_of_isWeaklyHarmonicOn {d : ℕ} {Q : HCPolySupport.TriadicCube d} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (f : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (h : Support.IsWeaklyHarmonicOn (HCPolySupport.openCubeSet Q) f) : HCPolySupport.Book.Ch03.IsConstantCoeffForcedEquation Q (scalarComparator hsigma0) f fun (x : HCPolySupport.Vec d) => 0

The frozen statement's harmonicity is the development's.

Support.IsWeaklyHarmonicOn is −Δv = 0 weakly; the coarse-graining chain uses Ch03.IsConstantCoeffForcedEquation at the scalar comparator σ Id with zero force. For a positive scalar comparator the two are the same condition: the scalar factors out of the weak identity.

3. The identification

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_sub_weaklyHarmonic_eq_harmonicCorrector {d : ℕ} [NeZero d] {sigma0 : ℝ} (hsigma0 : 0 < sigma0) {n m : ℤ} {x : HCPolySupport.Vec d} {W : Set (HCPolySupport.Vec d)} (hW : W = HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) (hsub : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (v : HCPolySupport.H1Function W) (w : HCPolySupport.H10Function W) (hharm : Support.IsWeaklyHarmonicOn W v) (hval : ∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun y - w.toFun y) (hgrad : ∀ (y : HCPolySupport.Vec d), v.grad y = u.grad y - w.grad y) : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2 (Support.normalizedVolumeMeasureOn W) = MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => (harmonicCorrector (scalarComparator hsigma0) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsub))).toFun y) 2 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d n))

The interior clause's left-hand side, in the child's own frame.

For every pair (v, w) the frozen theorem quantifies over — v weakly harmonic on the child window W = x + □_n, v = u − w with w ∈ H¹₀(W) — the anchor's own left-hand norm equals the normalized L² norm of the constructed harmonic corrector of the transported solution u_tilde = u(· + x):

  ‖u − v‖_{L²(W)}  =  ‖u(·+x) − v⋆‖_{L²(□_n)} ,
      v⋆ = harmonicReplacement (σ Id) u_tilde .

This is an exact identity. The comparator scale σ > 0 is free: harmonicity does not see it (§2), so the same v⋆ serves every positive scalar background.