MeanControlReduction #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The mean comparison, step 2: the homogenization-error split, and its loop-free #
account
What is proved #
The single number S is controlled by the homogenization error. That
mechanism is reduced here to its exact arithmetic skeleton and machine-checked.
With
ρ = u − h , V₁ = the covering cube c+□_{n+2} ,
V₂ = the boundary-flush cube of MeanControlWindowCube ,
W = the frozen window (z+□_{n+3}) ∩ □_m ⊇ V₁ ∪ V₂ ,
and comparators v (any function on V₂; intended: the Δ-harmonic
replacement of u there) and h (intended: the Δ-harmonic replacement of the
datum h), the module proves
S = |⨍_{V₁} ρ|
≤ (r₁ + r₂)·‖ρ − (ρ)_W‖_{L²(W)} (§1, §4: two window transfers)
+ ‖u − v‖_{L²(V₂)} (the homogenization error)
+ ‖h − h‖_{L²(V₂)} (the datum comparator, data-only)
+ |⨍_{V₂} (v − h)| , (§2: THE remaining scalar)
‖(v − h) − (v − h)_{V₂}‖_{L²(V₂)}
≤ 2‖u − v‖ + 2‖h − h‖ + ‖u − (u)_{V₂}‖ + ‖h − (h)_{V₂}‖ (§3, §5)
What this buys, and what remains #
Every summand except the last is a frozen-statement leg or a legal data step:
the window oscillation of ρ splits into the frozen leg ‖u − (u)_W‖ and the
datum oscillation ‖h − (h)_W‖ (the mean-zero Poincaré on the datum), and
‖h − h‖ is a Dirichlet-comparison step on
the datum alone. The single remaining analytic obligation is
|⨍_{V₂} (v − h)| ≤ C(d) · ‖(v − h) − (v − h)_{V₂}‖_{L²(V₂)}
for the Δ-harmonic difference v − h on the boundary-flush cube V₂,
whose trace vanishes on the face V₂ shares with ∂□_m (that face exists by
MeanControlWindowCube.wellPlacedCentre_faceLevel, and u − h ∈ H¹₀(□_m)).
That obligation is a statement about Δ-harmonic functions and Lebesgue
measure alone (the comparator class of BoundaryLaneMaxPrinciple), so flat
estimates suffice for it. §6 records the arithmetic that converts the
boundary-trace form of that obligation into the stated form.
0. Elementary identities for the normalized average #
The volume average of a constant is that constant.
The normalized seminorm of a constant is its absolute value.
The volume average is additive on integrable summands.
Subtracting a constant shifts the volume average by that constant.
1. The two-window mean transfer #
SlopeStabilityEndpoints provides abs_volumeAverage_sub_average_le so the
mean-control and Campanato branches share the same estimate.
The mean transfer.
For a subwindow V ⊆ W, the gap between the two normalized means is at most the
oscillation of f on the big window, at the square root of the volume ratio.
No equation, no coefficient field: Jensen on V followed by the volume-ratio
comparison of the normalized seminorms.
2. The split through the comparators #
The split.
u − h = (u − v) + (h − h) + (v − h) pointwise, so the mean of u − h over
the flush cube is controlled by the homogenization error ‖u − v‖, the datum
comparison ‖h − h‖, and the mean of the comparator difference v − h.
The first two summands are the pieces the proved machinery prices; the third is the single remaining analytic obligation, and it is a statement about the comparators alone.
3. The oscillation of a comparator #
The comparator's oscillation, in terms of the original's.
‖v − (v)_V‖ ≤ 2‖u − v‖ + ‖u − (u)_V‖: the comparator oscillates no more than
the original does, up to twice the comparison error. The proof is Minkowski
with the constant (u)_V inserted, plus Jensen on the mean gap; mean-minimality
is deliberately not used, so that the module needs no Pythagoras identity and
its import cone stays minimal.
The oscillation of a difference splits into the two oscillations.
4. The composite reduction #
5. The loop-free certificate #
The remaining obligation's own oscillation carries no S.
The oscillation of the comparator difference v − h on the flush cube is
bounded by twice the two comparison errors plus the oscillations of u and of
the datum h — and by nothing else.