IncrementLpGain #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The partition-average gain for the stream-increment L^p mass #
This module supplies the conditional large-window concentration kernel used
toward e.kl.bounds.large (ABK26): CoarseGraining's partition-average
fluctuation theorem
isBigO_gammaSigma_restrictionCenteredDescendantAverage_of_restrictionUnitRangeDependentLaw
is applied to the per-subcube L^p mass of a finite stream increment, and its
conclusion is transported back to the shell-sequence sample space in exactly
the head-plus-tail shape that
Provider/Stream/IncrementLp.streamIncrementLpNorm_head_tail_of_mass_head_tail
consumes.
The scale obstruction and the partition normalization #
CoarseGraining's theorem carries hn : 0 ≤ n on its subcube scale, because
it reaches a descendant cube from the origin cube by an integer
translation. Under it, the source's scale-m subcubes are replaced by the
slightly coarser scale-(m+c) subcubes, and the partition gain becomes
3^{-(d/2)(l-m-c)} = 3^{(d/2)c} * 3^{-(d/2)(l-m)},
i.e. the printed gain with a dimensional constant 3^{(d/2)c}. This is the `l
= m + c
regime; the complementary regimel < m + cis *not* treated here: there the partition is empty ande.kl.bounds.largereduces to the proved`l-uniforme.kmn.boundswith aC(d)-enlarged amplitude, which belongs to the assembly ofl.km.kn.Lp.estimates. The window binderhsl : m + c <= lbelow is an implementation branch condition, not a premise of the source theorem.IncrementLpLarge.lean` later combines this branch with the complementary regime and discharges the centering input.
What is proved #
dilateCube,cubeSet_dilateCube,descendantsAtDepth_dilateCube,descendantsAtScale_originCube_eq_image_dilateCube— the triadic dilation dictionary matchingsmulRegon the carrier.regFieldLpMass_smulReg— the cubeL^pmass is dilation covariant.descendantAverage_regFieldLpMassRep_eq_streamIncrementLpMass— the exact identification: at a partition-rescaled increment field, CoarseGraining's descendant partition average of the measurable representative is the cube massstreamIncrementLpMass p l n m omega.isBigOWith_comp_of_isBigO_map— transport of a weak-Orlicz tail bound along a push-forward.isBigOWith_gammaSigma_streamIncrementLpMass_sub_originMean— the deliverable: theGamma_sigmabound with the geometric partition gain for the centered cube mass, on the shell-sequence sample space.streamIncrementLpMass_head_tail— its packaging asmass <= H + TwithT >= 0andTinO_{Gamma_sigma}of the gain, the exact input ofstreamIncrementLpNorm_head_tail_of_mass_head_tail.
References #
- ABK26,
e.kl.bounds.large;e.kmn.bounds;p.concentration; the cutoff range. Provider/Stream/IncrementLaw.lean(incrementPartitionScale,partitionStreamIncrementLawand its two structural assumptions),Provider/Stream/IncrementConcentration.lean(the deterministic descendant identity),Provider/Stream/IncrementMassRepresentative.lean(the measurable local representative).
Triadic dilation #
The triadic dilation of a cube by the factor 3^s: the same index at a
scale shifted by s.
Equations
Instances For
The dilation dictionary on cube realizations.
The partition dictionary. The scale-s subcubes of the origin cube at
scale l are the triadic dilations by 3^s of the scale-0 subcubes of the
origin cube at scale l - s.
Dilation covariance of the cube L^p mass #
The cube L^p mass is dilation covariant: rescaling the field is the
same as rescaling the observation set.
The representative at a partition-rescaled increment #
At a triadically rescaled stream increment the measurable representative on a
cube is the cube average of the increment L^p density on the dilated cube.
The cube mass of a stream increment is the cube average of its density.
The exact identification. At a partition-rescaled increment field
CoarseGraining's descendant partition average of the measurable representative
is the cube mass of the increment on cu_l.
Transport of a weak-Orlicz tail bound along a push-forward #
A Psi tail bound for a measurable observable of a push-forward law is the
same bound for its composition with the (measurable) push-forward map.
The partition-average gain on the shell-sequence sample space #
The CoarseGraining partition-average fluctuation theorem, applied to the
increment mass. All three structural hypotheses (stationarity, unit-range
dependence) and all three regularity hypotheses (locality, translation
covariance, measurability) of the cube observable are discharged by the proved
Provider/Stream/IncrementLaw.lean and
Provider/Stream/IncrementMassRepresentative.lean.
The centered descendant average of the representative, read at a sample.
The origin-cube centering constant is the expected cube mass at the single
scale m + c.
The deliverable. On the shell-sequence sample space the cube L^p mass
of the increment on cu_l is, up to the deterministic head
E[⨍_{cu_{m+c}} |k_m - k_n|^p], of size O_{Gamma_sigma} of the partition gain
3^{-(d/2)(l-m-c)} times the origin-cube amplitude.
The head-plus-tail packaging. These are four of the five inputs of
streamIncrementLpNorm_head_tail_of_mass_head_tail (a nonnegative
deterministic head, a nonnegative tail, the pointwise mass bound, and the
Gamma_sigma tail bound with the partition gain); the fifth, hK : 0 ≤ K, is
supplied at the call site.