MeanFinalPointwise

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

(A), step 1: the near-face elimination for a face-odd harmonic function

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

for w Δ-harmonic on the boundary-flush cube K and vanishing on the face K shares with the frontier. This module carries its pointwise half.

The mechanism ('s, at a general face level)

Write ρ for the reflection in the face hyperplane {yᵢ = a} and let G = W − β where W is odd about the face — so that G satisfies the reflection identity G ∘ ρ + G = −2β, an identity carrying no information by itself. Harmonicity enters through a second-order Taylor comparison along the normal, applied twice:

• to the pair (y, ρ y), whose displacement is 2s·eᵢ with s = a − yᵢ;
• to the pair (y, y − w·eᵢ), whose displacement is −w·eᵢ.

The first, combined with the reflection identity, gives |β + G y + s·γ| ≤ 2 M w² where γ is the (unknown) normal derivative of G at y; the second gives |G(y − w·eᵢ) − G y + w·γ| ≤ M w² and therefore pins γ down to O(M w). Eliminating γ — legitimate because t = s/w ∈ (0,1], which is exactly why the comparison point is taken at the fixed signed depth w rather than at a depth proportional to s — leaves

  |β| ≤ 2 |G y| + |G (y − w·eᵢ)| + 3 M w² .

• the "even part" is a constant β (the mean), not the even part of an affine competitor, so the reflection identity is taken as a hypothesis at the single point y rather than derived from a global affine splitting;
• the depth w is signed, so the same statement serves an upper face (w > 0) and a lower face (w < 0) with no case split — only the ratio t = s/w ∈ (0,1] is constrained;
• the Taylor set T is an arbitrary convex set, not the x-window's taylorLo/taylorHi box, so the estimate is available at the flush cube of MeanControlWindowCube, whose centre is z and whose face may be either.

References

• ABK26, l.harmonic.approximation.good.scales, Step 2; l.excess.decay.good.scales.

1. The signed depth ratio

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sq_le_sq_of_div_mem {s w : ℝ} (h0 : 0 < s / w) (h1 : s / w ≤ 1) : s ^ 2 ≤ w ^ 2

If 0 < s/w ≤ 1 then s and w have the same sign and s² ≤ w².

2. The two-point Taylor elimination

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.abs_le_pointwise_of_reflectionIdentity {d : ℕ} {i : Fin d} {a : ℝ} {T : Set (HCPolySupport.Vec d)} (hT : Convex ℝ T) {G : HCPolySupport.Vec d → ℝ} {beta M w : ℝ} (hharm : ∀ z ∈ T, InnerProductSpace.HarmonicAt (G ∘ ⇑toEuc.symm) (toEuc z)) (hMb : ∀ z ∈ T, ‖fderiv ℝ (fderiv ℝ (G ∘ ⇑toEuc.symm)) (toEuc z)‖ ≤ M) {y : HCPolySupport.Vec d} (hyT : y ∈ T) (hrT : HCPolySupport.coordFaceReflection a i y ∈ T) (hpT : y - w • HCPolySupport.basisVec i ∈ T) (hrefl : G (HCPolySupport.coordFaceReflection a i y) + G y = -2 * beta) (h0 : 0 < (a - y i) / w) (h1 : (a - y i) / w ≤ 1) : |beta| ≤ 2 * |G y| + |G (y - w • HCPolySupport.basisVec i)| + 3 * M * w ^ 2

The near-face elimination, at a general face level and a signed depth.

Let G be classically harmonic on a convex set T with Hessian bounded by M there, and let y ∈ T satisfy the reflection identity G (ρ y) + G y = −2β for the reflection ρ in {yᵢ = a}. If both the reflected point ρ y and the pushed point y − w·eᵢ lie in T, and the signed depth ratio (a − yᵢ)/w lies in (0, 1], then the constant β is priced pointwise by the two values of G and a quadratic Hessian remainder:

  |β| ≤ 2 |G y| + |G (y − w·eᵢ)| + 3 M w² .

No continuity of G at the face and no membership hypothesis beyond the three listed points is used.