SharpFramedAfterBandScale

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

Saturated after-band scale with the global frame retained

The ordinary after-band term is priced here at the exact streamIncrementLpNormScale M 4 (ell + k₀) L. In particular, its squared scale retains the saturation factor min 1 (M.gamma * (L - (ell + k₀))); it is never relaxed to the linear factor M.gamma * (L - (ell + k₀)).

The final identities specialize the observation-to-layer frame at a strict descendant and expose the complete exponent after multiplication by the seam factor. These declarations are internal conditional obligations.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandExactScale {d : ℕ} (M : ABKModel d) (ell : ℤ) (k₀ : ℕ) (L : ℤ) : ℝ

The exact Gamma₂ scale of the rebased after-band term. The cancellation of the two k₀ powers is built into the displayed gauge, while the stream increment scale itself remains unchanged.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandExactScale_nonneg {d : ℕ} (M : ABKModel d) (ell : ℤ) (k₀ : ℕ) (L : ℤ) : 0 ≤ probeSharpAfterBandExactScale M ell k₀ L

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_probeSharpAfterBandTerm_exactScale {d : ℕ} (M : ABKModel d) (m ell : ℤ) (k₀ : ℕ) (L : ℤ) : Measurable (CoarseEllipticity.probeSharpAfterBandTerm M m ell k₀ L)

The after-band random variable is measurable at the exact scale.

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_probeSharpAfterBandTerm_exactScale {d : ℕ} (M : ABKModel d) {m ell L : ℤ} {k₀ : ℕ} (hL : ell + ↑k₀ < L) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (CoarseEllipticity.probeSharpAfterBandTerm M m ell k₀ L) (probeSharpAfterBandExactScale M ell k₀ L)

The exact after-band term has a Gamma₂ bound without replacing the stream increment scale by a square-root gap.

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_one_probeSharpAfterBandTerm_sq_exactScale {d : ℕ} (M : ABKModel d) {m ell L : ℤ} {k₀ : ℕ} (hL : ell + ↑k₀ < L) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.CutoffSample d) => CoarseEllipticity.probeSharpAfterBandTerm M m ell k₀ L omega ^ 2) (probeSharpAfterBandExactScale M ell k₀ L ^ 2)

Squaring the exact Gamma₂ estimate gives the exact Gamma₁ scale.

theorem Algsuperdiff.Section3.Provider.Multiscale.streamIncrementLpNormScale_four_eq_waveSharpUpperConst_min {d : ℕ} (M : ABKModel d) (n L : ℤ) : Stream.streamIncrementLpNormScale M 4 n L = waveSharpUpperConst d * min √M.gamma⁻¹ √(↑L - ↑n) * 3 ^ (M.gamma * ↑L)

At p = 4, the exact stream-norm scale is the point-scale carrier with its min untouched.

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandExactScale_eq_min {d : ℕ} (M : ABKModel d) {ell L : ℤ} {k₀ : ℕ} : probeSharpAfterBandExactScale M ell k₀ L = waveSharpUpperConst d * √M.gamma * min √M.gamma⁻¹ √(↑L - ↑(ell + ↑k₀)) * 3 ^ (M.gamma * (↑L - ↑ell))

Exact normalization of the after-band scale: the short-gap saturation and the global exponent are both visible.

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandExactScale_sq_eq_min {d : ℕ} (M : ABKModel d) {ell L : ℤ} {k₀ : ℕ} (hL : ell + ↑k₀ < L) : probeSharpAfterBandExactScale M ell k₀ L ^ 2 = waveSharpUpperConst d ^ 2 * min 1 (M.gamma * (↑L - ↑(ell + ↑k₀))) * 3 ^ (2 * M.gamma * (↑L - ↑ell))

The squared exact scale is exactly a dimension constant times the saturated short-gap factor and the full global exponent.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedAfterBandMultiplier {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (omega : Cutoff.CutoffSample d) : ℝ

The random multiplier carried by the framed after-band square inside one sharp Whitney layer.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedAfterBandMultiplier_nonneg {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpFramedAfterBandMultiplier M root E b k₀ n i omega

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_probeSharpFramedAfterBandMultiplier {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) : Measurable (probeSharpFramedAfterBandMultiplier M root E b k₀ n i)

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedAfterBandMultiplier_descendant_eq {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) (E b : ℝ) (k₀ n : ℕ) (omega : Cutoff.CutoffSample d) : probeSharpFramedAfterBandMultiplier M R.scale E b k₀ n (m - 1) omega = 3 ^ (M.gamma * (↑(Percolation.hsep M R.scale E b omega) - (↑k + ↑n + ↑⌈b * (1 - b)⁻¹ * ↑n⌉₊ + ↑k₀)))

At a descendant observed from scale m - 1, the retained frame cancels one of the two seam powers exactly.