TwoLaneCoverDepth #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The deterministic lane-separated cover of the observation cube #
This module is the deterministic half of the lane-separated observation-scale
transport of Provider/Homogenization/TwoLaneCoverTransport.lean; it is
separated to keep each Lean file focused and below the repository line limit.
It contains no probability: every statement here is a pointwise inequality at
a fixed sample point, and the two cell families it is run against are
arbitrary.
Fix a coefficient cutoff scale L, an observation cube square_m and two cell
families g, h on the cubes. The squared raw homogenization error of
square_m, read at the discount 1/8, expands into weighted depth layers.
The first m - L layers are coarse: each is dominated by the maximum, over
that layer's parents, of the average of the cell family over their scale-L
descendants (laneParentAverage). The remaining layers are fine: they sit
below the cutoff scale and are dominated, with a geometrically summable factor
(laneFineFactor), by the maximum of the cell family over all scale-L cells
of the observation cube (laneCellSup). Every step is monotone in the cell
family and the two maxima are subadditive, so a cover of the squared raw cell
errors by g + h splits the whole deterministic bound into one cover
functional per lane (laneTotal). That is the content of the endpoint of this
module, cutoffHomogenizationErrorRaw_sq_le_laneTotal_add.
No comparator change occurs anywhere: the coefficient cutoff is a_L and the
normalizer is sigmabar_L at the cell scale, at every intermediate scale and
at the observation cube. The discounts t = 1/8 at the observation cube and
u = 1/16 at the cells are the ones fixed by the corrected Step 4 of
p.combine.under.S; see the References of
Provider/Homogenization/TwoLaneCoverTransport.lean.
The declarations below are local Provider results.
Two elementary facts about the finite averages and suprema of the cover #
The cover functional of one lane #
The layer-ell parent maximum of the descendant averages of one cell
family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coarse part of the cover functional: the first m - L layers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The maximum of one cell family over all scale-L cells of the observation
cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The geometric factor paid by the fine tail below the cutoff scale.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full cover functional of one cell family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The deterministic cover, split over the two lanes #
The squared raw cutoff error of a scale-L cell, read at the cell
window 1/16.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The layer-ell term of the weighted-depth expansion of the squared raw
error of the observation cube.
Equations
- One or more equations did not get rendered due to their size.