GammaTenInteriorFamily #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Besov envelope of Step 2 on an arbitrary sub-mesh #
ABK26, Step 2 of l.approximate.recurrence.formula,
e.lower.bound.oscillations.
Why the proved grid device is not enough #
The envelope device of Closure.GammaTenEnvelopeInputGrid is set up on the
full mesh descendantsAtDepth Q j, so its per-depth input D i is the
full-mesh grid fourth moment of the oscillation cells at depth i. The
depth-indexed endpoints of
Closure.GammaTenDepthOscillation are stated on the interior mesh
interiorMesoCubeGrid d K (nmesh - i) (m - h - 1), the carrier, and --- as
that module records --- the boundary-strip transfer of
LocalizationOscillationFullMesh does not survive the depth index: the
missing fraction d 3^{(m-h)-K} is the same at every depth, while the Besov
tower's own weights 2^{i+1} 3^{4 s i} grow geometrically, so a
depth-independent remainder is not summable.
This module removes that obstruction by running the same envelope device on
an arbitrary sub-family I of the mesh. Nothing analytic changes: the
proved exists_grid_pathwise_envelope_of_monotone is already stated at an
arbitrary Finset (TriadicCube d); what has to be redone is only the fold,
because the proved fold identifies avsum_{R in mesh} avsum_{R' in desc(R,i)}
with the refined mesh average through
descendantsAverage_add_eq_descendantsAverage_descendantsAverage, an identity
that holds for the full mesh only.
The replacement is the finite combinatorics of this module: the depth-i
descendant families of distinct cells of a common mesh are disjoint
(disjoint_descendantsAtDepth_of_ne), so for a nonnegative cell functional the
sub-family's iterated sum is dominated by any grid T containing all those
descendants (sum_descendantsAtDepth_le_of_subset), at the explicit cardinality
cost |T| / (|I| 3^{d i}) (cubeFamilyAverage_descendantsAverage_le). On the
interior mesh that cost is 1 / (1 - boundary fraction), i.e. below 2 under
the recurrence's own large-cube gate, and it is carried in the statement.
What is proved #
disjoint_descendantsAtDepth_of_ne--- distinct cells of a common mesh have disjoint depth-idescendant families.sum_descendantsAtDepth_le_of_subset--- the iterated sum over a sub-family is below the sum over any grid containing the descendants.cubeFamilyAverage_descendantsAverage_le--- the same with the two averages normalized, with the cardinality ratio explicit.cubeFamilyAverage_integral_pow_four_oscMajorant_le_family--- the fold at an arbitrary sub-family: the sub-family average of the fourth moment ofClosure.GammaTenEnvelopeInputGrid.oscMajorant, bounded by the weighted sum over depths of per-depth inputs read at the sub-family itself.integrable_pow_four_oscMajorant_family--- the fourth power of the majorant is integrable at every cell of the sub-family.exists_besovEnvelope_of_family_depth_oscillation--- the composite: the envelope on the sub-family, from per-depth sub-family oscillation moments alone.
Binders #
Measurability and fourth-power integrability of the oscillation cells at the
descendants of the sub-family's cells, the L^2 membership of the field there,
the common scale of the sub-family and the per-depth bounds. No smallness gate,
no geometry beyond the triadic mesh, and nothing about the corrector or the
coefficient field occurs.
Scope #
Internal Provider infrastructure for the Step-2 fluctuation estimate. There is
no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2,e.lower.bound.oscillations,e.nablaw.oscillations.
Disjointness of the descendant families of a common mesh #
Distinct cells of a common mesh have disjoint descendant families. Two
distinct cells of descendantsAtDepth Q j have disjoint open cubes, and a cube
is contained in the open cube of each of its ancestors, so a common descendant
would have empty open cube. Unconditional.
The iterated sum over a sub-mesh is below the sum over any grid containing the descendants. Unconditional for a family nonnegative on that grid.
The sub-mesh depth average, against a containing grid.
If every depth-i descendant family of the sub-mesh I proves inside the grid
T, and f is nonnegative on T, then the sub-mesh average of the depth-i
descendant averages is below rho times the T-average, rho being any bound
for the cardinality ratio |T| / (|I| 3^{d i}).
Unconditional finite combinatorics.
The fold at an arbitrary sub-mesh #
The grid fourth moment of the majorant, folded over depths, at an arbitrary sub-mesh.
The fold of Closure.GammaTenEnvelopeInputGrid.oscMajorant whose per-depth
input D i is read at the sub-mesh I itself rather than at the full mesh.
The proof is the full-mesh one with the closing identity
descendantsAverage_add_eq_descendantsAverage_descendantsAverage --- which is
available only on the full mesh --- replaced by the hypothesis hD.
on hint, the standing fourth-power integrability of the oscillation cells at
the descendants of the sub-mesh, and on the per-depth bounds hD.
The fourth power of the majorant is integrable at every cell of the sub-mesh, by domination through the fold.
on the measurability and the fourth-power integrability of the oscillation cells at the descendants of that cell.
The composite #
The Besov envelope of Step 2 on an arbitrary sub-mesh, from per-depth sub-mesh oscillation moments alone.
The envelope device of Closure.GammaTenEnvelopeInputGrid, run at an arbitrary
family I of cells of a common scale nbase. The conclusion is the exact
shape Closure.ClosureInteriorSplit.ClosureInteriorBesovEnvelopeInput
consumes.
on hscale, hmeascell, hintcell, hmem2, hD and hsum.