ResidueInterface

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

The boundary scalar S at the harmonic-approximation residue interface

What is proved

exists_scalarControl_boundaryBranch_comparator re-cuts the proved composed scalar theorem of the boundary lane's seal chain so that its third right-hand summand is no longer the gradient residue 3^n·Σᵢ‖∂ᵢu‖_{L²(K')} but the strictly smaller harmonic-approximation error at the flush sub-cube: the theorem now produces a Δ-harmonic comparator w = u + ρ, ρ ∈ H¹₀(K'), together with the estimate

  S ≤ C(d) · ( ‖u − (u)_{W'}‖_{L²(W')}                        (the FIRST leg)
             + 3^n · Σᵢ ‖∂ᵢh‖_{L²(W')}                        (the FIFTH leg)
             + ‖u − w‖_{L²(K')} )                             (the RESIDUE)

with V₁ the anchor's covering cube, W' = (z+□_{n+3}) ∩ □_m the frozen window, K' = flushSubCentre z m n i σ + □_n the flush scale-n sub-cube, and C(d) explicit and dimension-only.

Why the re-cut matters

The proved statement's residue has exactly one coefficient-free producer, the Dirichlet-principle Poincaré ‖u − w‖ ≤ C·3^n·Σᵢ‖∂ᵢu‖ of SealComparator; composing it with the fitted boundary Caccioppoli costs √(σ/ν). Exposing the comparator instead removes that composition from the interface: ‖u − w‖_{L²(K')} is literally an instance of the harmonic-approximation display the development's anchor proves, read at the flush sub-cube K' instead of at the anchor's child cube x+□_n. Applying SealComparator's Poincaré bound to the produced w recovers the proved statement verbatim, so this is a strict sharpening — nothing is lost. The ∀-budget form consumed by the assembly is ResidueBudget.exists_scalarControl_of_boundaryBranch_harmonicResidue.

References

• ABK26, l.harmonic.approximation.good.scales, Step 2.

1. The scalar control at the harmonic-approximation residue interface

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundaryComparatorOscillationAndMeanBounds (d : ℕ) {n m : ℤ} {z : HCPolySupport.Vec d} {i : Fin d} {σ : ℝ} (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : have c' := flushSubCentre z m n i σ; MeasurableSet ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) → 0 < (MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))).toReal → MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ≠ ⊤ → ∀ (wu wh : HCPolySupport.H1Function (HCPolySupport.translateSet c' (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))), MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) → MeasureTheory.MemLp u.toFun 2 (MeasureTheory.volume.restrict ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) → MeasureTheory.MemLp h.toFun 2 (MeasureTheory.volume.restrict ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) → MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => wu.toFun y) 2 (MeasureTheory.volume.restrict ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) → MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => wh.toFun y) 2 (MeasureTheory.volume.restrict ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) → MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => u.toFun y - wu.toFun y) 2 (MeasureTheory.volume.restrict ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) → MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => h.toFun y - wh.toFun y) 2 (MeasureTheory.volume.restrict ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) → ((Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => wu.toFun x - wh.toFun x - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => wu.toFun y - wh.toFun y) ≤ (((2 * Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => u.toFun x - wu.toFun x) + 2 * Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => h.toFun x - wh.toFun x) + Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => u.toFun x - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) u.toFun) + Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => h.toFun x - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) h.toFun) ∧ |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => u.toFun x - h.toFun x| ≤ ((Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => u.toFun x - wu.toFun x) + Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => wh.toFun x - h.toFun x) + |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (x : HCPolySupport.Vec d) => wu.toFun x - wh.toFun x|

Comparator oscillation and mean bounds from finite local L² data.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_grad_le_anchorWindow {d : ℕ} {n m : ℤ} {z c : HCPolySupport.Vec d} (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hsub : (fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hWpos : 0 < (MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))).toReal) (hKpos : 0 < (MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))).toReal) (hKtop : MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ≠ ⊤) (i : Fin d) : (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => h.grad y i) ≤ √(27 ^ d) * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => h.grad y i) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal

Transport each gradient coordinate from a contained cube to its anchor window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_sub_comparator_le_of_gradient_transport {d : ℕ} {n : ℤ} {c : HCPolySupport.Vec d} {u w : HCPolySupport.Vec d → ℝ} {g : Fin d → HCPolySupport.Vec d → ℝ} {K : ℝ} {B : Fin d → ℝ} (hbound : (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u y - w y) ≤ comparatorPoincareConst d * 3 ^ n * ∑ i : Fin d, Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) (g i)) (hgrad : ∀ (i : Fin d), Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) (g i) ≤ K * B i) : (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u y - w y) ≤ comparatorPoincareConst d * K * 3 ^ n * ∑ i : Fin d, B i

Sum transported gradients in the comparator Poincaré estimate.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_volumeAverage_comparator_sub_le_of_setEq {d : ℕ} {U V W A : Set (HCPolySupport.Vec d)} {CA : ℝ} (hUV : U = V) (w0 : HCPolySupport.H10Function W) (hmean : ∀ (v : HCPolySupport.H1Function U), Support.IsWeaklyHarmonicOn U v → ∀ (ru rh : HCPolySupport.H10Function U), (∀ (y : HCPolySupport.Vec d), v.toFun y = w0.toFun y + ru.toFun y - rh.toFun y) → |HCPolySupport.volumeAverage A v.toFun| ≤ CA * Support.normalizedL2On A fun (y : HCPolySupport.Vec d) => v.toFun y - HCPolySupport.volumeAverage A v.toFun) (wu wh : HCPolySupport.H1Function V) (ru rh : HCPolySupport.H10Function V) (hu : Support.IsWeaklyHarmonicOn V wu) (hh : Support.IsWeaklyHarmonicOn V wh) (hsplit : ∀ (y : HCPolySupport.Vec d), wu.toFun y - wh.toFun y = w0.toFun y + ru.toFun y - rh.toFun y) : |HCPolySupport.volumeAverage A fun (y : HCPolySupport.Vec d) => wu.toFun y - wh.toFun y| ≤ CA * Support.normalizedL2On A fun (y : HCPolySupport.Vec d) => wu.toFun y - wh.toFun y - HCPolySupport.volumeAverage A fun (x : HCPolySupport.Vec d) => wu.toFun x - wh.toFun x

Transport a harmonic comparator difference before applying a mean estimate.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.comparator_mean_bound_of_legs {CA a b c p q X H NU NH P A B child comp osc oscU oscH : ℝ} (hCA : 0 ≤ CA) (htri : P ≤ A + B + child) (hA : A ≤ a * X) (hB : B ≤ b * H) (hsplit : child ≤ NU + NH + comp) (hcomp : comp ≤ CA * osc) (hosc : osc ≤ 2 * NU + 2 * NH + oscU + oscH) (hoscU : oscU ≤ 2 * q * X) (hoscH : oscH ≤ p * H) (hNH : NH ≤ c * H) : P ≤ (a + CA * (2 * q)) * X + (b + c + CA * (2 * c + p)) * H + (1 + CA * 2) * NU

Assemble comparator oscillation, approximation, and parent-to-child mean bounds.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_sub_average_le_of_gradient_transport {d : ℕ} {n m : ℤ} {c : HCPolySupport.Vec d} (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hK'm : (fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {K : ℝ} {B : Fin d → ℝ} (hgradHtrans : ∀ (i : Fin d), (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => h.grad y i) ≤ K * B i) : (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => h.toFun y - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) h.toFun) ≤ HCPolySupport.unitMeanZeroPoincareConst d * K * 3 ^ n * ∑ i : Fin d, B i

Mean-zero Poincaré on a translated cube after transporting each gradient coordinate.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_sub_average_le_twice_sqrt_ratio {d : ℕ} {m : ℤ} {A W : Set (HCPolySupport.Vec d)} {R : ℝ} (hK'meas : MeasurableSet A) (hKW' : A ⊆ W) (hW'm : W ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hW'pos : 0 < (MeasureTheory.volume W).toReal) (hK'pos : 0 < (MeasureTheory.volume A).toReal) (hK'top : MeasureTheory.volume A ≠ ⊤) (hW'top : MeasureTheory.volume W ≠ ⊤) (hR : (MeasureTheory.volume W).toReal / (MeasureTheory.volume A).toReal ≤ R) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : (Support.normalizedL2On A fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage A u.toFun) ≤ 2 * √R * Support.normalizedL2On W fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage W u.toFun

Restricting to a finite positive-volume set controls its centered norm by its volume ratio against the containing window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.residueInterface_comparatorIntegrability {d : ℕ} {U K V W : Set (HCPolySupport.Vec d)} (u h : HCPolySupport.H1Function U) (hKU : K ⊆ U) (hVU : V ⊆ U) (hWU : W ⊆ U) (wu wh : HCPolySupport.H1Function K) : MeasureTheory.MemLp u.toFun 2 (MeasureTheory.volume.restrict K) ∧ MeasureTheory.MemLp h.toFun 2 (MeasureTheory.volume.restrict K) ∧ MeasureTheory.MemLp u.toFun 2 (MeasureTheory.volume.restrict V) ∧ MeasureTheory.MemLp h.toFun 2 (MeasureTheory.volume.restrict V) ∧ MeasureTheory.MemLp u.toFun 2 (MeasureTheory.volume.restrict W) ∧ MeasureTheory.MemLp wu.toFun 2 (MeasureTheory.volume.restrict K) ∧ MeasureTheory.MemLp wh.toFun 2 (MeasureTheory.volume.restrict K) ∧ MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => u.toFun x - wu.toFun x) 2 (MeasureTheory.volume.restrict K) ∧ MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => h.toFun x - wh.toFun x) 2 (MeasureTheory.volume.restrict K)

Square-integrability of two functions, their local comparators and their differences. The three comparison regions can be arbitrary subsets of the original domain.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_scalarControl_boundaryBranch_comparator (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {n m : ℤ} {x z : HCPolySupport.Vec d} {i : Fin d} {σ : ℝ}, n + 2 ≤ m → x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → σ = 1 ∨ σ = -1 → wellPlacedHalfGap m (n + 2) < σ * z i → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.HasZeroTraceDifferenceOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u h → ∃ (w : HCPolySupport.H1Function (HCPolySupport.translateSet (flushSubCentre z m n i σ) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) (rho : HCPolySupport.H10Function (HCPolySupport.translateSet (flushSubCentre z m n i σ) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))), Support.IsWeaklyHarmonicOn (HCPolySupport.translateSet (flushSubCentre z m n i σ) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) w ∧ (∀ (y : HCPolySupport.Vec d), w.toFun y = u.toFun y + rho.toFun y) ∧ (∀ (y : HCPolySupport.Vec d), w.grad y = u.grad y + rho.grad y) ∧ |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - h.toFun y| ≤ C * ((MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + 3 ^ n * ∑ i' : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => h.grad y i') 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u.toFun y - w.toFun y) ∧ (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u.toFun y - w.toFun y) ≤ comparatorPoincareConst d * 3 ^ n * ∑ i' : Fin d, Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u.grad y i'

The boundary scalar S, composed, with the residue exhibited as the harmonic-approximation error at the flush sub-cube.

S = |⨍_{V₁}(u−h)| is priced, coefficient-free, by the frozen shape, the frozen shape, and any real R dominating ‖u − w‖_{L²(K')} for every Δ-harmonic comparator w = u + ρ, ρ ∈ H¹₀(K').