StepSevenMean #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
t.regularity Step 7d: the hmean producer, and the chain without hmean #
The gap this module closes #
oscTrunc ≤ Cmean · ( (3^{Q.scale})^{-1} · osc_{L²}(Q; u) )
as a hypothesis of the narrowed Step-7d chain.
Producers do exist, in two steps, at Cmean = √(3^d):
normalizedL2On_image_add_sub_average_le_cubeBesovOscillation(the off-grid recovery at constant1) — the translated cube's mass against the origin-cube oscillation of the translated sample.
This module composes them (stepSevenHmean_of_sandwich) and proves the
narrowed chain with hmean gone
(exists_stepSevenEnd_chain_of_lambda_hmeanFree).
The carriers, and where the two constants come from #
At the scale normalization Q = originCube d k (k = m'-1 at the consumption
site) with the sample translated by c:
oscTrunc = 3^{-k}‖u - (u)_{(z+□_k)∩□_m}‖_{L²((z+□_k)∩□_m)} (the tex's LHS)
≤ 3^{d/2} · 3^{-k}‖u - (u)_{c+□_k}‖_{L²(c+□_k)} (sandwich)
≤ 3^{d/2} · 3^{-k}·osc_{L²}(□_k; u(·+c)) . (cost 1)
So Cmean = √(3^d) and nothing else enters.
What is still the caller's #
The five integrability binders of the two proved atoms (w and w² on both
windows, and the mean-subtracted square on the sandwich cube) and the sandwich
inclusion hST — the latter is StepSevenSelectionData.upper_sandwich_in at
k = m'-1, so it is free at the selection. The three measure-theoretic side
conditions of the sandwich cube (measurability, positive volume, finite volume)
are discharged here
rather than carried: a translate of the open cube is open and has volume
3^{dk}.
References #
- ABK26, Step 7d.
1. The sandwich cube's measure-theoretic data, discharged #
The translated open cube is measurable.
The translated open cube has finite volume.
The translated open cube has positive volume 3^{dk}.
2. The hmean producer #
3^{-k}‖u - (u)_{(z+□_k)∩□_m}‖_{L²((z+□_k)∩□_m)}
≤ √(3^d) · ( 3^{-k} · osc_{L²}(□_k; u(·+c)) ) ,
which is the hmean slot of the Step-7d chain at Cmean = √(3^d) and Q = originCube d k. Two proved atoms composed, nothing else.
The Step-7d transported oscillation is nonnegative — the chain's hoscTrunc at
the concrete carrier, so the caller need not supply it.
3. The narrowed chain, with hmean gone #
Step 7d end to end with hcg, hembed, hbridge AND hmean discharged.
exists_stepSevenEnd_chain_of_lambda_gen fed by stepSevenHmean_of_sandwich, at
Cmean = √(3^d) and the concrete transported oscillation
oscTrunc = 3^{-k}‖u - (u)_{(z+□_k)∩□_m}‖_{L²((z+□_k)∩□_m)} .
hoscTrunc is discharged too (it is a product of nonnegatives at the concrete
carrier). The remaining conditional inputs are hlambda
(e.lambda.stability.applied) and the Step-7c gradient display hgrad;
everything else is the caller's geometry, integrability, or the printed
nonnegativity data.