SharpMeanSplitWave

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeStreamIncrementLpNorm_originCube_eq_probe {d : ℕ} {p : ℝ} (hp : 0 < p) (m n L : ℤ) (omega : Cutoff.ShellSeq d) : Stream.cubeStreamIncrementLpNorm p (HCPolySupport.originCube d m) n L omega = Stream.streamIncrementLpNorm p m n L omega

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpAfterBandTerm {d : ℕ} (M : ABKModel d) (m ell : ℤ) (k₀ : ℕ) (L : ℤ) (omega : Cutoff.CutoffSample d) : ℝ

The sharp ordinary wave term above the tuned deep band, rebased to the lower edge of that band.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpAfterBandTerm_nonneg {d : ℕ} (M : ABKModel d) (m ell : ℤ) (k₀ : ℕ) (L : ℤ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpAfterBandTerm M m ell k₀ L omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveGauge_mul_upperNorm_eq_probe {d : ℕ} (M : ABKModel d) (m ell : ℤ) (k₀ : ℕ) (L : ℤ) (omega : Cutoff.CutoffSample d) : √M.gamma * 3 ^ (-(M.gamma * ↑ell)) * Stream.streamIncrementLpNorm 4 m (ell + ↑k₀) L ↑omega = probeSharpAfterBandTerm M m ell k₀ L omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.streamIncrementLpNorm_deepBand_waveGauge_origin_probe {d : ℕ} (M : ABKModel d) (m ell : ℤ) {k₀ N g₀ : ℕ} (hk₀ : 2 ≤ k₀) (hN : k₀ < 3 ^ N) (hm : m = ell + ↑k₀ + ↑g₀) : (∀ (omega : Cutoff.CutoffSample d), √M.gamma * 3 ^ (-(M.gamma * ↑ell)) * Stream.streamIncrementLpNorm 4 m ell (ell + ↑k₀) ↑omega ≤ waveBandMean (probeDeepBandMeanAmplitude d) M.gamma k₀ + probeDeepBandGaugedTail M (HCPolySupport.originCube d m) ell k₀ N omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (probeDeepBandGaugedTail M (HCPolySupport.originCube d m) ell k₀ N) (probeDeepBandGaugedFluct M ell k₀ g₀) ∧ Measurable (probeDeepBandGaugedTail M (HCPolySupport.originCube d m) ell k₀ N)

The exact root-cube deep-band split. The carrier gap g₀ is left explicit so a Whitney layer can instantiate it with n + ⌈b(1-b)⁻¹n⌉₊.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveL4Amplitude_le_head_deepBand_sharpUpper_tail_probe {d : ℕ} (M : ABKModel d) {m : ℤ} {E b : ℝ} {ell L : ℤ} {k₀ N g₀ : ℕ} (hk₀ : 2 ≤ k₀) (hN : k₀ < 3 ^ N) (hm : m = ell + ↑k₀ + ↑g₀) (htopL : ell + ↑k₀ ≤ L) (omega : Cutoff.CutoffSample d) : √M.gamma * 3 ^ (-(M.gamma * ↑ell)) * Stream.streamIncrementLpNorm 4 m (ell - ↑(Percolation.hsep M m E b omega)) L ↑omega ≤ Multiscale.waveHeadTerm M m E b ell omega + waveBandMean (probeDeepBandMeanAmplitude d) M.gamma k₀ + probeDeepBandGaugedTail M (HCPolySupport.originCube d m) ell k₀ N omega + probeSharpAfterBandTerm M m ell k₀ L omega + Multiscale.waveTailTerm M m E b m ell omega

The wave-gauged amplitude split at a root cube: random-depth head, mean-split deep band, sharp macroscopic upper increment, and random-depth tail. No grid maximum or translated-cube penalty is introduced.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpLayerAnchor (m : ℤ) (b : ℝ) (k₀ n : ℕ) : ℤ

The lower anchor scale for a sharp layer with its prescribed separation gap.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpLayerAnchor m b k₀ n = m - ↑n - ↑⌈b * (1 - b)⁻¹ * ↑n⌉₊ - ↑k₀

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpLayerGap (b : ℝ) (n : ℕ) : ℕ

The natural-number separation gap assigned to a sharp layer.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpLayerGap b n = n + ⌈b * (1 - b)⁻¹ * ↑n⌉₊

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpLayerAnchor_scale_eq (m : ℤ) (b : ℝ) (k₀ n : ℕ) : m = probeSharpLayerAnchor m b k₀ n + ↑k₀ + ↑(probeSharpLayerGap b n)

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_gammaSigma_one_probeDeepBandGaugedTail_origin_sq {d : ℕ} (M : ABKModel d) (m ell : ℤ) {k₀ g₀ : ℕ} (hk₀ : 2 ≤ k₀) (hm : m = ell + ↑k₀ + ↑g₀) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.CutoffSample d) => probeDeepBandGaugedTail M (HCPolySupport.originCube d m) ell k₀ k₀ omega ^ 2) (probeDeepBandGaugedFluct M ell k₀ g₀ ^ 2)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveTailGainScale_nonneg_probe (d : ℕ) (b sigma sigma2 : ℝ) (lout ell : ℤ) : 0 ≤ Multiscale.waveTailGainScale d b sigma sigma2 lout ell

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_gammaSigma_probeWaveTailTerm_sq_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} {E sigma sigma2 b : ℝ} (hd2 : 2 ≤ d) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hsigma2 : 0 < sigma2) (hb0 : 0 < b) (hb1 : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ E) (hgammaE : M.gamma ≤ E ^ (-5)) (lout ell : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (sigma2 / (2 + sigma2))) (fun (omega : Cutoff.CutoffSample d) => Multiscale.waveTailTerm M m E b lout ell omega ^ 2) (Multiscale.waveTailGainScale d b sigma sigma2 lout ell ^ 2)

The active squared wave-tail leg derived from the raw bad-event gates.