IncrementLaw

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The restriction-law carrier of a finite stream increment

The node e.kl.bounds.large of l.km.kn.Lp.estimates (ABK26) improves the l-uniform estimate e.kmn.bounds on scales larger than 3^m by combining the finite-range assumption a.j.frd with the concentration proposition p.concentration, applied to the average of the cube L^p masses over the scale-m subcubes of cu_l.

The concentration input available to this repository is CoarseGraining's partition-average fluctuation theorem isBigO_gammaSigma_restrictionCenteredDescendantAverage_of_restrictionUnitRangeDependentLaw, whose hypotheses are structural assumptions on a restriction-lane law P: Ch04.RestrictionCoeffLaw d, namely RestrictionStationaryLaw P and RestrictionUnitRangeDependentLaw P. This module supplies the law and both structural assumptions for the stream increment k_m - k_n = sum_{k in (n,m]} j_k.

What is proved

• scaledStreamIncrementLaw_stationary_real, scaledStreamIncrementLaw_stationary — the joint, multi-shell translation covariance, at an arbitrary nonzero spatial rescaling. This is not the one-shell statement map_shellObservable_translate_eq: it is the whole-sequence invariance Cutoff.sequenceLaw_stationary (derived in the Cutoff layer from the independence of the shells, the marginal scaling law and (J1)), pushed through the exact commutation translateReg_finiteShellIncrement.
• scaledStreamIncrementLaw_unitRangeDependent — CoarseGraining's unit-range dependence for a rescaled increment law. Any factor leaving strict bridge slack for the literal range sqrt(d) 3^m turns that range into a strictly sub-unit one, exactly as Cutoff.RangeNormalization does for the coefficient cutoff a_m.
• partitionStreamIncrementLaw, the rescaling the partition step can actually use, at the depth Cutoff.cutoffNormalizationDepth d m; partitionStreamIncrementLaw_stationary and partitionStreamIncrementLaw_unitRangeDependent are the two structural assumptions the concentration theorem asks for, at that law.
• scaledStreamIncrementLaw_eq_map, the un-normalization dictionary: every statement about a rescaled law is a statement about x |-> (k_m - k_n)(r x) under M.P.

References

• ABK26, e.kl.bounds.large; l.km.kn.Lp.estimates; the cutoff range; a.j.frd.
• Algsuperdiff/Section3/Cutoff/RangeNormalization.lean, the same normalization for the coefficient cutoff.

Continuity of the increment in the space variable

theorem Algsuperdiff.Section3.Provider.Stream.continuous_finiteShellIncrement_entry {d : ℕ} (omega : Cutoff.ShellSeq d) (n m : ℤ) (i j : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => (Cutoff.finiteShellIncrement omega n m).toFun x i j

Every matrix entry of a finite stream increment is continuous in the point: the increment is a finite sum of shells, each of which is a continuous matrix-valued path.

Joint multi-shell translation covariance

theorem Algsuperdiff.Section3.Provider.Stream.translateReg_finiteShellIncrement {d : ℕ} (z : HCPolySupport.Vec d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : HCPolySupport.translateReg z (Cutoff.finiteShellIncrement omega n m) = Cutoff.finiteShellIncrement (Frozen.Assumptions.ShellField.translateSequence z omega) n m

Translating the whole shell sequence translates the finite increment. This is the multi-shell covariance the concentration input needs: it is an exact identity of regular coefficient fields, uniform in the finitely many shells (n, m].

Locality of the increment in the lower-shell stream

theorem Algsuperdiff.Section3.Provider.Stream.measurable_finiteShellIncrement_local {d : ℕ} (n m : ℤ) (U : Set (HCPolySupport.Vec d)) : Measurable fun (omega : Cutoff.ShellSeq d) => Cutoff.finiteShellIncrement omega n m

A finite stream increment reads only shells of index at most m, so it is measurable for the lower-shell integral-local sigma-field at scale m. No relation between n and m is needed: for m < n the increment is the zero field.

Spatially rescaled increment laws

CoarseGraining's restriction-lane partition-average concentration theorem isBigO_gammaSigma_restrictionCenteredDescendantAverage_of_restrictionUnitRangeDependentLaw requires its subcube scale to be >= 0, because its proof reaches a descendant cube from the origin cube by an integer translation and RestrictionStationaryLaw is integer-translation invariance only. The normalization depth of Cutoff.RangeNormalization (which sends the range sqrt(d) 3^m below 1) sends the scale-m subcubes to a strictly negative scale, so it cannot be the normalization used for the partition step.: NO rescaling clears the CoarseGraining 0 ≤ n restriction for the manuscript's own scale-m subcubes — unit range needs r > 2·sqrt(d)·3^m > 3^m while nonnegative subcube scale needs r ≤ 3^m; the two are incompatible. The factor may be a negative power of 3, outside the range of restrictionScaleNormalizedLaw : ℕ → _.

Both normalizations are therefore obtained here from one statement about an arbitrary nonzero spatial scaling smulReg r.

noncomputable def Algsuperdiff.Section3.Provider.Stream.scaledStreamIncrementLaw {d : ℕ} (M : ABKModel d) (n m : ℤ) (r : ℝ) (hr : r ≠ 0) : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d

The increment law spatially rescaled by a nonzero factor r: the law of x |-> (k_m - k_n)(r x).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.scaledStreamIncrementLaw_eq_map {d : ℕ} (M : ABKModel d) (n m : ℤ) {r : ℝ} (hr : r ≠ 0) : scaledStreamIncrementLaw M n m r hr = MeasureTheory.Measure.map (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.smulReg r hr (Cutoff.finiteShellIncrement omega n m)) ↑M.P

instance Algsuperdiff.Section3.Provider.Stream.scaledStreamIncrementLaw_isProbabilityMeasure {d : ℕ} (M : ABKModel d) (n m : ℤ) (r : ℝ) (hr : r ≠ 0) : MeasureTheory.IsProbabilityMeasure (scaledStreamIncrementLaw M n m r hr)

theorem Algsuperdiff.Section3.Provider.Stream.translateReg_smulReg {d : ℕ} {r : ℝ} (hr : r ≠ 0) (z : HCPolySupport.Vec d) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.translateReg z (HCPolySupport.smulReg r hr a) = HCPolySupport.smulReg r hr (HCPolySupport.translateReg (r • z) a)

Translation commutes with spatial rescaling on the carrier.

theorem Algsuperdiff.Section3.Provider.Stream.scaledStreamIncrementLaw_stationary_real {d : ℕ} (M : ABKModel d) (n m : ℤ) {r : ℝ} (hr : r ≠ 0) (z : HCPolySupport.Vec d) : MeasureTheory.Measure.map (HCPolySupport.translateReg z) (scaledStreamIncrementLaw M n m r hr) = scaledStreamIncrementLaw M n m r hr

Real-translation stationarity survives every spatial rescaling, because the increment law is invariant under all real translations.

theorem Algsuperdiff.Section3.Provider.Stream.scaledStreamIncrementLaw_stationary {d : ℕ} (M : ABKModel d) (n m : ℤ) {r : ℝ} (hr : r ≠ 0) : HCPolySupport.Book.Ch04.RestrictionStationaryLaw (scaledStreamIncrementLaw M n m r hr)

CoarseGraining's restriction-stationarity predicate for every rescaled increment law.

Unit-range dependence of the normalized increment law

theorem Algsuperdiff.Section3.Provider.Stream.scaledStreamIncrementLaw_unitRangeDependent {d : ℕ} (M : ABKModel d) (n m : ℤ) {r : ℝ} (hr : r ≠ 0) (hrpos : 0 < r) (hslack : Cutoff.cutoffNaturalRange d m < r * (1 - 2 * Cutoff.cutoffBridgeEpsilon)) : HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw (scaledStreamIncrementLaw M n m r hr)

CoarseGraining's exact unit-range dependence for a rescaled increment law.

The increment k_m - k_n reads only shells of index at most m, whose joint integral-local information has literal Euclidean range sqrt(d) 3^m (Cutoff.indep_lowerShellLocalSigma_of_cutoff_separation). Rescaling by any factor r that leaves strict epsilon = 1/4 bridge slack for that range turns it into a strictly sub-unit range, which is CoarseGraining's RestrictionUnitRangeDependentLaw after the thickening bridge. This is the RestrictionUnitRangeDependentLaw hypothesis of isBigO_gammaSigma_restrictionCenteredDescendantAverage_of_restrictionUnitRangeDependentLaw.

The partition normalization

CoarseGraining's restriction-lane partition theorem needs its subcube scale to be ≥ 0. The scale that achieves this sends the scale-m subcubes to scale 0, i.e. rescales by 3^{m+c} where 3^c > 2 sqrt(d); this is in general not a rescaling by a natural power of 3, so it is outside the range of restrictionScaleNormalizedLaw.

noncomputable def Algsuperdiff.Section3.Provider.Stream.incrementPartitionShift (d : ℕ) : ℕ

The dimensional shift c: the least triadic depth with 3^c > 2 sqrt(d).

Equations

• Algsuperdiff.Section3.Provider.Stream.incrementPartitionShift d = Algsuperdiff.Section3.Cutoff.cutoffNormalizationDepth d 0

noncomputable def Algsuperdiff.Section3.Provider.Stream.incrementPartitionScale (d : ℕ) (m : ℤ) : ℝ

The partition normalization factor 3^{m+c}: it sends the scale-m subcubes of the partition to unit cubes and the literal range sqrt(d) 3^m strictly below the bridge budget.

Equations

• Algsuperdiff.Section3.Provider.Stream.incrementPartitionScale d m = 3 ^ (m + ↑(Algsuperdiff.Section3.Provider.Stream.incrementPartitionShift d))

theorem Algsuperdiff.Section3.Provider.Stream.incrementPartitionScale_pos (d : ℕ) (m : ℤ) : 0 < incrementPartitionScale d m

theorem Algsuperdiff.Section3.Provider.Stream.incrementPartitionScale_ne_zero (d : ℕ) (m : ℤ) : incrementPartitionScale d m ≠ 0

theorem Algsuperdiff.Section3.Provider.Stream.incrementPartitionScale_strict_slack (d : ℕ) (m : ℤ) : Cutoff.cutoffNaturalRange d m < incrementPartitionScale d m * (1 - 2 * Cutoff.cutoffBridgeEpsilon)

noncomputable def Algsuperdiff.Section3.Provider.Stream.partitionStreamIncrementLaw {d : ℕ} (M : ABKModel d) (n m : ℤ) : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d

The partition-normalized increment law: the law of x |-> (k_m - k_n)(3^{m+c} x), under which the scale-(m+c) subcubes of cu_l become the scale-0 descendants of cu_{l-m-c} (the scale-m subcubes land at scale -c;).

Equations

• One or more equations did not get rendered due to their size.

instance Algsuperdiff.Section3.Provider.Stream.partitionStreamIncrementLaw_isProbabilityMeasure {d : ℕ} (M : ABKModel d) (n m : ℤ) : MeasureTheory.IsProbabilityMeasure (partitionStreamIncrementLaw M n m)

theorem Algsuperdiff.Section3.Provider.Stream.partitionStreamIncrementLaw_stationary {d : ℕ} (M : ABKModel d) (n m : ℤ) : HCPolySupport.Book.Ch04.RestrictionStationaryLaw (partitionStreamIncrementLaw M n m)

theorem Algsuperdiff.Section3.Provider.Stream.partitionStreamIncrementLaw_unitRangeDependent {d : ℕ} (M : ABKModel d) (n m : ℤ) : HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw (partitionStreamIncrementLaw M n m)