DeepBandGroup

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

def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex (top : ℤ) (k₀ p : ℕ) : ℤ

The upper scale index of a truncated geometric band.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex top k₀ p = top - ↑(min (3 ^ p - 1) k₀)

def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandLength (k₀ p : ℕ) : ℕ

The number of scales in a truncated geometric band.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandLength k₀ p = min (3 ^ (p + 1) - 1) k₀ - min (3 ^ p - 1) k₀

def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandGroups (top : ℤ) (k₀ N : ℕ) : Finset ℕ

The nonempty truncated bands among the first N bands.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex_le (top : ℤ) (k₀ p : ℕ) : probeBandIndex top k₀ p ≤ top

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex_succ_le (top : ℤ) (k₀ p : ℕ) : probeBandIndex top k₀ (p + 1) ≤ probeBandIndex top k₀ p

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex_of_cover (top : ℤ) {k₀ N : ℕ} (hN : k₀ < 3 ^ N) : probeBandIndex top k₀ N = top - ↑k₀

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex_sub (top : ℤ) (k₀ p : ℕ) : probeBandIndex top k₀ p - probeBandIndex top k₀ (p + 1) = ↑(probeBandLength k₀ p)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandLength_le (k₀ p : ℕ) : probeBandLength k₀ p ≤ 2 * 3 ^ p

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.streamIncrementLpNorm_self_probe {d : ℕ} {p : ℝ} (hp : 0 < p) (l a : ℤ) (omega : Cutoff.ShellSeq d) : Stream.streamIncrementLpNorm p l a a omega = 0

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.streamIncrementLpNorm_probeBand_ladder {d : ℕ} {p : ℝ} (hp : 1 ≤ p) (l top : ℤ) (k₀ N : ℕ) (omega : Cutoff.ShellSeq d) : Stream.streamIncrementLpNorm p l (probeBandIndex top k₀ N) top omega ≤ ∑ r ∈ Finset.range N, Stream.streamIncrementLpNorm p l (probeBandIndex top k₀ (r + 1)) (probeBandIndex top k₀ r) omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.streamIncrementLpNorm_probeBand_ladder_of_cover {d : ℕ} {p : ℝ} (hp : 1 ≤ p) (l ell : ℤ) {k₀ N : ℕ} (hN : k₀ < 3 ^ N) (omega : Cutoff.ShellSeq d) : Stream.streamIncrementLpNorm p l ell (ell + ↑k₀) omega ≤ ∑ r ∈ Finset.range N, Stream.streamIncrementLpNorm p l (probeBandIndex (ell + ↑k₀) k₀ (r + 1)) (probeBandIndex (ell + ↑k₀) k₀ r) omega

@[simp]

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.mem_probeBandGroups {top : ℤ} {k₀ N r : ℕ} : r ∈ probeBandGroups top k₀ N ↔ r ∈ Finset.range N ∧ probeBandIndex top k₀ (r + 1) < probeBandIndex top k₀ r

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.zero_mem_probeBandGroups (top : ℤ) {k₀ N : ℕ} (hk₀ : 2 ≤ k₀) (hN : k₀ < 3 ^ N) : 0 ∈ probeBandGroups top k₀ N

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex_eq_of_not_mem_groups {top : ℤ} {k₀ N r : ℕ} (hr : r ∈ Finset.range N) (hnot : r ∉ probeBandGroups top k₀ N) : probeBandIndex top k₀ (r + 1) = probeBandIndex top k₀ r

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeStreamIncrementLpNorm_self_probe {d : ℕ} {p : ℝ} (hp : 0 < p) (Q : HCPolySupport.TriadicCube d) (a : ℤ) (omega : Cutoff.ShellSeq d) : Stream.cubeStreamIncrementLpNorm p Q a a omega = 0

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeStreamIncrementLpNorm_probeBand_ladder_of_cover {d : ℕ} {p : ℝ} (hp : 1 ≤ p) (Q : HCPolySupport.TriadicCube d) (ell : ℤ) {k₀ N : ℕ} (hN : k₀ < 3 ^ N) (omega : Cutoff.ShellSeq d) : Stream.cubeStreamIncrementLpNorm p Q ell (ell + ↑k₀) omega ≤ ∑ r ∈ probeBandGroups (ell + ↑k₀) k₀ N, Stream.cubeStreamIncrementLpNorm p Q (probeBandIndex (ell + ↑k₀) k₀ (r + 1)) (probeBandIndex (ell + ↑k₀) k₀ r) omega

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandTail {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (top : ℤ) (k₀ N : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The sum of fourth-moment stream tails over the selected deep bands.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_cubeStreamIncrementLpTail_rpow_cutoff_probe {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 0 < p) (Q : HCPolySupport.TriadicCube d) (n m : ℤ) : Measurable fun (omega : Cutoff.CutoffSample d) => Stream.cubeStreamIncrementLpTail M p Q n m ↑omega ^ p⁻¹

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandTail_measurable {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (top : ℤ) (k₀ N : ℕ) : Measurable (probeDeepBandTail M Q top k₀ N)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandTail_nonneg {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (top : ℤ) (k₀ N : ℕ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeDeepBandTail M Q top k₀ N omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeStreamIncrementLpNorm_deepBand_groupSplit_probe {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (ell : ℤ) {k₀ N : ℕ} (hk₀ : 2 ≤ k₀) (hN : k₀ < 3 ^ N) : (∀ (omega : Cutoff.CutoffSample d), Stream.cubeStreamIncrementLpNorm 4 Q ell (ell + ↑k₀) ↑omega ≤ ∑ r ∈ probeBandGroups (ell + ↑k₀) k₀ N, Stream.streamIncrementLpMassHead M 4 (probeBandIndex (ell + ↑k₀) k₀ (r + 1)) (probeBandIndex (ell + ↑k₀) k₀ r) ^ 4⁻¹ + probeDeepBandTail M Q (ell + ↑k₀) k₀ N omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (probeDeepBandTail M Q (ell + ↑k₀) k₀ N) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * ∑ r ∈ probeBandGroups (ell + ↑k₀) k₀ N, Stream.streamIncrementLpGainScale M 4 Q.scale (probeBandIndex (ell + ↑k₀) k₀ (r + 1)) (probeBandIndex (ell + ↑k₀) k₀ r) ^ 4⁻¹)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandLength_eq_zero {k₀ r : ℕ} (h : k₀ < 3 ^ r) : probeBandLength k₀ r = 0

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.sqrt_probeBandLength_le (k₀ r : ℕ) : √↑(probeBandLength k₀ r) ≤ √2 * √3 ^ r

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandMeanSumRaw (k₀ N : ℕ) : ∑ r ∈ Finset.range N, √↑(probeBandLength k₀ r) ≤ 3.7 * √↑k₀

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandMeanSum (t : ℝ) (k₀ N : ℕ) : ∑ r ∈ Finset.range N, √(min t ↑(probeBandLength k₀ r)) ≤ 3.7 * √↑k₀

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandLength_zero {k₀ : ℕ} (hk₀ : 2 ≤ k₀) : probeBandLength k₀ 0 = 2

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandGainSum (t : ℝ) (N g₀ : ℕ) {k₀ : ℕ} (hk₀ : 2 ≤ k₀) {q : ℝ} (hq0 : 0 ≤ q) (hq : q ≤ 0.76) : ∑ r ∈ Finset.range N, √(min t ↑(probeBandLength k₀ r)) * q ^ (g₀ + (3 ^ r - 1)) ≤ 3 * (q ^ g₀ * √↑(probeBandLength k₀ 0))

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandUnitGain (d : ℕ) : ℝ

The gain from one scale in the deep-band estimate.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandUnitGain d = 3 ^ (-↑d / 8)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandBlockGain (d : ℕ) (g : ℤ) : ℝ

The gain over a block of scales in the deep-band estimate.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandBlockGain d g = 3 ^ (-↑d / 8 * ↑g)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandUnitGain_nonneg (d : ℕ) : 0 ≤ probeBandUnitGain d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandBlockGain_natCast (d g : ℕ) : probeBandBlockGain d ↑g = probeBandUnitGain d ^ g

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandUnitGain_le {d : ℕ} (hd : 2 ≤ d) : probeBandUnitGain d ≤ 0.76

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandMeanAmplitude (d : ℕ) : ℝ

The dimension-dependent mean amplitude for the deep-band estimate.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandMeanAmplitude d = 3.7 * Algsuperdiff.Section3.Provider.CoarseEllipticity.deepBandAmplitude d 4

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandMeanAmplitude_nonneg (d : ℕ) : 0 ≤ probeDeepBandMeanAmplitude d

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandRawMean (d : ℕ) (gamma : ℝ) (top : ℤ) (k₀ : ℕ) : ℝ

The unnormalized mean budget for a finite deep-band range.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandRawMean d gamma top k₀ = Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandMeanAmplitude d * √↑k₀ * 3 ^ (gamma * ↑top)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandGainRootConst (d : ℕ) : ℝ

The fourth-root gain constant used to bound deep-band fluctuations.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandRawFluct (d : ℕ) (gamma : ℝ) (top : ℤ) (g₀ : ℕ) : ℝ

The unnormalized fluctuation budget after the initial depth cutoff.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.streamIncrementLpMassHead_fourth_eq_probe {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) : Stream.streamIncrementLpMassHead M 4 n m ^ 4⁻¹ = deepBandAmplitude d 4 * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.streamIncrementLpGainScale_fourth_eq_probe {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (l : ℤ) : Stream.streamIncrementLpGainScale M 4 l n m ^ 4⁻¹ = probeDeepBandGainRootConst d * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m) * probeBandBlockGain d (l - m)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.three_rpow_gamma_probeBandIndex_le {gamma : ℝ} (hgamma : 0 ≤ gamma) (top : ℤ) (k₀ r : ℕ) : 3 ^ (gamma * ↑(probeBandIndex top k₀ r)) ≤ 3 ^ (gamma * ↑top)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.sum_probeBandMassHead_fourth_le {d : ℕ} (M : ABKModel d) (top : ℤ) (k₀ N : ℕ) : ∑ r ∈ probeBandGroups top k₀ N, Stream.streamIncrementLpMassHead M 4 (probeBandIndex top k₀ (r + 1)) (probeBandIndex top k₀ r) ^ 4⁻¹ ≤ probeDeepBandRawMean d M.gamma top k₀

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeBandIndex_of_mem_groups {top : ℤ} {k₀ N r : ℕ} (hr : r ∈ probeBandGroups top k₀ N) : probeBandIndex top k₀ r = top - ↑(3 ^ r - 1)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandGainRootConst_nonneg (d : ℕ) : 0 ≤ probeDeepBandGainRootConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaTriangle_mul_sum_probeBandGain_fourth_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (top : ℤ) (k₀ N g₀ : ℕ) (hk₀ : 2 ≤ k₀) (hQ : Q.scale = top + ↑g₀) : HCPolySupport.IndependentSums.gammaTriangleConst 2 * ∑ r ∈ probeBandGroups top k₀ N, Stream.streamIncrementLpGainScale M 4 Q.scale (probeBandIndex top k₀ (r + 1)) (probeBandIndex top k₀ r) ^ 4⁻¹ ≤ probeDeepBandRawFluct d M.gamma top g₀

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeStreamIncrementLpNorm_deepBand_groupMeanSplit_probe {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (ell : ℤ) {k₀ N g₀ : ℕ} (hk₀ : 2 ≤ k₀) (hN : k₀ < 3 ^ N) (hQ : Q.scale = ell + ↑k₀ + ↑g₀) : (∀ (omega : Cutoff.CutoffSample d), Stream.cubeStreamIncrementLpNorm 4 Q ell (ell + ↑k₀) ↑omega ≤ probeDeepBandRawMean d M.gamma (ell + ↑k₀) k₀ + probeDeepBandTail M Q (ell + ↑k₀) k₀ N omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (probeDeepBandTail M Q (ell + ↑k₀) k₀ N) (probeDeepBandRawFluct d M.gamma (ell + ↑k₀) g₀) ∧ Measurable (probeDeepBandTail M Q (ell + ↑k₀) k₀ N)

8. The single wave-gauge application

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandGaugedTail {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (ell : ℤ) (k₀ N : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The grouped deep-band tail after applying exactly the wave gauge from the upper ellipticity argument.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandGaugedTail_nonneg {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (ell : ℤ) (k₀ N : ℕ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeDeepBandGaugedTail M Q ell k₀ N omega

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeDeepBandGaugedFluct {d : ℕ} (M : ABKModel d) (ell : ℤ) (k₀ g₀ : ℕ) : ℝ

The exact Γ₂ scale of the wave-gauged grouped tail.

Equations

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

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

Applying the wave gauge once turns the grouped deterministic head into the exact waveBandMean slot, while preserving the Γ₂ tail certificate.