TwoLaneCoverConstant #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The dimension-only cover constant of one exponent #
This module carries the scale bookkeeping 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. Nothing here
depends on the lane: the Orlicz exponent sigma is an arbitrary positive real
parameter and the cell family is arbitrary.
Two things are recorded. First, the layer scales of the deterministic cover of
Provider/Homogenization/TwoLaneCoverDepth.lean at a general exponent
sigma: laneDepthScale is the layer weight of the coarse expansion times the
finite-maximum cost (3 max(1, log N))^{1/sigma} of that layer's parent
generation times the triangle constant gammaTriangleConst sigma, and
laneFineDepthScale is its fine-tail analogue. Both are strictly positive --
which is what the countable triangle inequality demands of its scales -- and
both are summable, because the geometric layer weight beats the polynomial cost
(1 + ell)^{1/sigma}. The resulting dimension-only constant is
laneCoverConst d sigma, which is at least 1 by construction. Second, the
measurability in the sample of the three cover functionals, which the
probabilistic aggregation needs and which is discharged internally, never as a
binder.
The declarations below are local Provider results.
The dimension-only cover constant of one exponent #
The layer scale of the cover at the exponent sigma: the geometric weight
of the layer, the finite-maximum cost of that layer's parent generation, and
the triangle constant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dimension-only cover constant of the exponent sigma.
Equations
- One or more equations did not get rendered due to their size.