CoarseMeanComparison #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The mean-comparison chain, formalized and orientation-checked #
Nothing here imports that file, and nothing here claims the anchor or any source node.
The mechanism under test #
The mechanism under test, stated verbatim: "since the average of a function is
the unique constant c minimizing the L² norm of u − c, I think you can
compare u − (u) to u − (h) to u − h, the last bit costing exactly the ∇h
term."
- §1 Pythagoras — the exact identity, for
0 < |W| < ∞andf ∈ L²(W):‖f − c‖²_{L²(W)} = ‖f − (f)_W‖²_{L²(W)} + |(f)_W − c|². - §2 Mean-minimality — its immediate corollary
‖f − (f)_W‖ ≤ ‖f − c‖for every constantc, and the scalar half|(f)_W − c| ≤ ‖f − c‖. - §3 The author's chain, end to end:
|(u)_W − (h)_W| ≤ ‖u − h‖_{L²(W)} + ‖h − (h)_W‖_{L²(W)}, the last term discharged by the proved data Poincaré at the covering cube (§5). - §4 The reverse decomposition, which is what the boundary assembly's slot
actually consumes:
‖u − h‖_{L²(W)} ≤ ‖u − (u)_W‖ + |(u)_W − (h)_W| + ‖h − (h)_W‖.
Orientation finding (STOP, reported to the author) #
Write S := |(u)_W − (h)_W| (the residue at W = c + □_{n+2}), Osc:= ‖u − (u)_W‖_{L²(W)} (absorbed by the frozen leg through mean-minimality plus the
proved window transport) and Dat:= ‖h − (h)_W‖_{L²(W)} (absorbed by the
frozen leg through the proved data Poincaré). The boundary Caccioppoli's
parent-L² object is ‖u(·+c) − v_cc‖_{L²(cc)}, and (CoarseDatumPricing
having priced ‖v_cc − h‖) the one quantity still to bound is ‖u − h‖_{L²(cc)}.
The two machine-checked statements below are
§3 (author's chain) : S ≤ ‖u − h‖ + Dat
§4 (assembly's need): ‖u − h‖ ≤ Osc + S + Dat
They are the same inequality read in the two directions: §3 bounds S by
the very quantity the assembly must bound, and §4 bounds that quantity by S.
Chaining them is vacuous (‖u−h‖ ≤ Osc + ‖u−h‖ + 2·Dat). Mean-minimality
produces Osc ≤ ‖u − (h)_W‖, i.e. a lower bound on the quantity the slot
needs an upper bound for; Pythagoras turns that into the exact identity
‖u − (h)_W‖² = Osc² + S², which determines ‖u − (h)_W‖ from Osc and S
rather than bounding S.
Nothing here is forced and no substitute mechanism is attempted. The two
sides, verbatim, are the statements of
meanGap_le_normalizedL2On_sub_add_datumOscillation (§3, what the chain gives)
and normalizedL2On_sub_le_oscillation_add_meanGap_add_datumOscillation (§4,
what the slot needs, with S still present at coefficient 1).
1. Pythagoras in the normalized carrier #
Pythagoras on the normalized carrier.
For a window of positive finite volume and an L² function, the deviation from
any constant splits orthogonally into the oscillation and the mean gap:
‖f − c‖²_{L²(W)} = ‖f − (f)_W‖²_{L²(W)} + |(f)_W − c|² .
2. Mean-minimality and the scalar half #
Mean-minimality. The volume average is the L²(W)-minimizing constant:
the oscillation is at most the deviation from any constant. This is the author's
first comparison, and it is the step that lets the assembly replace the covering
cube's own mean by the frozen clause's (u)_{W'} at no cost.
The normalized seminorm of a constant is its absolute value.
3. The author's chain, end to end #
4. The reverse decomposition: what the assembly's slot consumes #
The assembly's slot.
‖u − h‖_{L²(W)}
≤ ‖u − (u)_W‖_{L²(W)} + |(u)_W − (h)_W| + ‖h − (h)_W‖_{L²(W)} ,
i.e. the boundary Caccioppoli's parent-L² object, after
CoarseDatumPricing has removed the ‖v_cc − h‖ leg, reduces to the frozen
leg (through mean-minimality and the proved window transport), the frozen leg
(through the data Poincaré) and the residue S = |(u)_W − (h)_W| at
coefficient 1.
Read together with §3 it shows the mean-comparison chain to be an identity in
disguise rather than a bound on S.