MeanFinalMeanBound

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

(A): the flush-cube mean bound

  |β| ≤ C · ‖W − β‖_{L²(K)}

for a function W odd about the face hyperplane {yᵢ = a} that the cube K shares with the boundary, and classically harmonic on a doubled window D ⊇ K. Applied with β = ⨍_K W this is exactly

  |⨍_K W| ≤ C(d) · ‖W − (W)_K‖_{L²(K)} ,

the statement that a Δ-harmonic function vanishing on a face of K cannot be close to a nonzero constant; the general-β form is what the composition actually uses.

The proof, in three moves

1. The pointwise near-face elimination (MeanFinalPointwise): at every point y of a thin slab S under the face, the reflection identity plus two second-order Taylor steps eliminate the unknown normal derivative and give |β| ≤ 2|G y| + |G(y − w·eᵢ)| + 3Mw² with G = W − β.
2. The slab average: normalizedL2On_mono_of_abs_le and Minkowski turn that into |β| ≤ 2‖G‖_{L²(S)} + ‖G‖_{L²(S − w·eᵢ)} + 3Mw², and both seminorms transfer to K at the volume ratio (|K|/|S|)^{1/2}.
3. The absorption: M is the interior Hessian bound of exists_hessian_normalizedL2On_bound on D, so 3Mw² carries the quadratically small factor w²; the doubled-window transfer of MeanFinalCore returns ‖G‖_{L²(D)} to 2‖G‖_{L²(K)} + 3|β|, and the room hypothesis 9·CH·r⁻¹·r⁻¹·RD·w² ≤ 1/2 absorbs the |β| that comes back.

The geometry is left abstract — four sets S ⊆ K ⊆ D, S ⊆ T ⊆ D with the inclusions each move uses — so that the same statement serves an upper and a lower flush face of MeanControlWindowCube: the sign of the face lives entirely in the signed depth w, and every hypothesis below is sign free.

References

• ABK26, l.harmonic.approximation.good.scales, Step 2 (boundary cubes).

1. A translated window has the same volume

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.image_sub_eq_preimage_add' {d : ℕ} (S : Set (HCPolySupport.Vec d)) (v : HCPolySupport.Vec d) : (fun (z : HCPolySupport.Vec d) => z - v) '' S = (fun (z : HCPolySupport.Vec d) => z + v) ⁻¹' S

Translating a window is a measure-preserving relabelling.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.volume_image_sub {d : ℕ} (S : Set (HCPolySupport.Vec d)) (v : HCPolySupport.Vec d) : MeasureTheory.volume ((fun (z : HCPolySupport.Vec d) => z - v) '' S) = MeasureTheory.volume S

The volume of a translated window.

2. The slab average

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.abs_le_slab_of_pointwise {d : ℕ} {i : Fin d} {w : ℝ} {S : Set (HCPolySupport.Vec d)} {G : HCPolySupport.Vec d → ℝ} {beta Mw : ℝ} (hSm : MeasurableSet S) (hSpos : 0 < (MeasureTheory.volume S).toReal) (hStop : MeasureTheory.volume S ≠ ⊤) (hGS : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict S)) (hGpush : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => G (y - w • HCPolySupport.basisVec i)) 2 (MeasureTheory.volume.restrict S)) (hMw : 0 ≤ Mw) (hpt : ∀ y ∈ S, |beta| ≤ 2 * |G y| + |G (y - w • HCPolySupport.basisVec i)| + Mw) : |beta| ≤ 2 * Support.normalizedL2On S G + Support.normalizedL2On ((fun (z : HCPolySupport.Vec d) => z - w • HCPolySupport.basisVec i) '' S) G + Mw

The slab average of the pointwise near-face bound.

If a constant β is dominated pointwise on S by 2|G| + |G(· − v)| + Mw, then it is dominated by the corresponding L²(S) seminorms.

3. (A)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_abs_le_normalizedL2On_of_faceOdd (d : ℕ) [NeZero d] : ∃ (CH : ℝ), 0 ≤ CH ∧ ∀ (i : Fin d) (a w r : ℝ) (K D S T : Set (HCPolySupport.Vec d)) (W : HCPolySupport.Vec d → ℝ) (beta RK RD : ℝ), (∀ (z : HCPolySupport.Vec d), W (HCPolySupport.coordFaceReflection a i z) = -W z) → MeasureTheory.MemLp W 2 (MeasureTheory.volume.restrict D) → InnerProductSpace.HarmonicOnNhd ((fun (y : HCPolySupport.Vec d) => W y - beta) ∘ ⇑toEuc.symm) (⇑toEuc '' D) → Convex ℝ T → T ⊆ D → S ⊆ K → K ⊆ D → (fun (z : HCPolySupport.Vec d) => z - w • HCPolySupport.basisVec i) '' S ⊆ K → (∀ y ∈ S, y ∈ T ∧ HCPolySupport.coordFaceReflection a i y ∈ T ∧ y - w • HCPolySupport.basisVec i ∈ T ∧ 0 < (a - y i) / w ∧ (a - y i) / w ≤ 1) → (∀ z ∈ T, Metric.ball z r ⊆ D) → 0 < r → (∀ y ∈ D, y ∈ K ∨ HCPolySupport.coordFaceReflection a i y ∈ K ∨ y i = a) → MeasurableSet S → MeasurableSet K → MeasurableSet D → MeasureTheory.volume D ≠ ⊤ → 0 < (MeasureTheory.volume S).toReal → 0 < (MeasureTheory.volume K).toReal → 0 < (MeasureTheory.volume D).toReal → (MeasureTheory.volume K).toReal ≤ (MeasureTheory.volume D).toReal → √((MeasureTheory.volume K).toReal / (MeasureTheory.volume S).toReal) ≤ RK → √((MeasureTheory.volume D).toReal / r ^ d) ≤ RD → 0 ≤ RD → 9 * (CH * r⁻¹ * r⁻¹ * RD * w ^ 2) ≤ 1 / 2 → |beta| ≤ (6 * RK + 12 * (CH * r⁻¹ * r⁻¹ * RD * w ^ 2)) * Support.normalizedL2On K fun (y : HCPolySupport.Vec d) => W y - beta

(A), the flush-cube mean bound.

Let W be odd about the face hyperplane {yᵢ = a}, square integrable on a doubled window D, and let G = W − β be classically harmonic on D. Let K ⊆ D be the cube, S ⊆ K a near-face slab whose translate by w·eᵢ also lies in K, and T a convex Taylor set containing S, its reflection and its translate, with a uniform ball of radius r inside D at each of its points. If D is covered — up to the face hyperplane — by K and the reflection of K, then

  |β| ≤ (6·RK + 12·CH·r⁻¹·r⁻¹·RD·w²) · ‖W − β‖_{L²(K)} ,

where bounds (|K|/|S|)^{1/2} bounds (|D|/rᵈ)^{1/2} is the dimensional constant of the interior Hessian estimate — provided the absorption has room, 9··r⁻¹·r⁻¹··w² ≤ 1/2.