SharpTailProbability

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

Almost-sure sharp shell rates at every crossover scale

The two Γ₂ shell estimates are grouped by square boxes in ℤ × ℤ. We square the normalized gauges, turning Γ₂ into Γ₁; the graded finite-envelope lemma then pays one linear factor for the row entropy. The original cube maximum already costs a square root of that row size. Taking the square root of the resulting envelope therefore gives exactly the first power of 2 + |n| + |ell|, with no additional power beyond that linear crossover weight.

noncomputable def Algsuperdiff.Section5.Field.sharpTailOrliczConst (d : ℕ) : ℝ

A dimension-only scale large enough for both one-shell Γ₂ estimates.

Equations

• Algsuperdiff.Section5.Field.sharpTailOrliczConst d = Real.exp 1 * Algsuperdiff.Section3.Cutoff.gaussianMaximumDimConst d + Algsuperdiff.Section3.Provider.Stream.shellW1InfConst d

theorem Algsuperdiff.Section5.Field.sharpTailOrliczConst_pos (d : ℕ) : 0 < sharpTailOrliczConst d

noncomputable def Algsuperdiff.Section5.Field.sharpValueRatio {d : ℕ} (gamma : ℝ) (n ell : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The value gauge divided by its exact shell amplitude.

Equations

• Algsuperdiff.Section5.Field.sharpValueRatio gamma n ell omega = Algsuperdiff.Section3.Cutoff.localCubeControl ell (↑omega n) / Real.rpow 3 (gamma * ↑n)

noncomputable def Algsuperdiff.Section5.Field.sharpGradientRatio {d : ℕ} (gamma : ℝ) (n ell : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The derivative gauge divided by its exact shell amplitude.

Equations

• Algsuperdiff.Section5.Field.sharpGradientRatio gamma n ell omega = Algsuperdiff.Section5.Field.sharpGradientGauge ell n omega / Real.rpow 3 ((gamma - 1) * ↑n)

theorem Algsuperdiff.Section5.Field.isBigOWith_gammaSigma_sharpValueRatio {d : ℕ} (M : Section3.ABKModel d) (n ell : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (sharpValueRatio M.gamma n ell) (sharpTailOrliczConst d * √(sharpTailWeight n ell))

The value ratio has a common Γ₂ scale bounded by the square root of the integer crossover weight.

theorem Algsuperdiff.Section5.Field.isBigOWith_gammaSigma_sharpGradientRatio {d : ℕ} (M : Section3.ABKModel d) (n ell : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (sharpGradientRatio M.gamma n ell) (sharpTailOrliczConst d * √(sharpTailWeight n ell))

The derivative ratio has the same common Γ₂ scale.

The joint square-box envelope

def Algsuperdiff.Section5.Field.sharpTailRow (k : ℕ) : Finset (Bool × ℤ × ℤ)

Both gauges over the square [-k,k]²; false is the value leg and true is the derivative leg.

Equations

• Algsuperdiff.Section5.Field.sharpTailRow k = Finset.univ.product ((Finset.Icc (-↑k) ↑k).product (Finset.Icc (-↑k) ↑k))

noncomputable def Algsuperdiff.Section5.Field.sharpTailSquaredObservable {d : ℕ} (gamma : ℝ) (_k : ℕ) (i : Bool × ℤ × ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The squared normalized observable used to turn the Γ₂ inputs into a Γ₁ row.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.sharpTailSquaredScale (d k : ℕ) : ℝ

A common deterministic Γ₁ scale for the squared observables in row k.

Equations

• Algsuperdiff.Section5.Field.sharpTailSquaredScale d k = (Algsuperdiff.Section5.Field.sharpTailOrliczConst d * √(2 + 2 * ↑k)) ^ 2

noncomputable def Algsuperdiff.Section5.Field.sharpTailEnvelope {d : ℕ} (M : Section3.ABKModel d) : Section3.Cutoff.CutoffSample d → ℝ

The explicit joint envelope whose finiteness supplies one sample constant for every shell/cube pair and both gauges.

Equations

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

theorem Algsuperdiff.Section5.Field.ae_sharpTailEnvelope_bound {d : ℕ} (M : Section3.ABKModel d) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (k : ℕ), ∀ i ∈ sharpTailRow k, sharpTailSquaredObservable M.gamma k i omega ≤ Section3.Provider.CoarseEllipticity.gradedFiniteEnvelopeScale 8 (sharpTailSquaredScale d) k * sharpTailEnvelope M omega

theorem Algsuperdiff.Section5.Field.sharpTailBounded_of_envelope {d : ℕ} (M : Section3.ABKModel d) (omega : Section3.Cutoff.CutoffSample d) (homega : ∀ (k : ℕ), ∀ i ∈ sharpTailRow k, sharpTailSquaredObservable M.gamma k i omega ≤ Section3.Provider.CoarseEllipticity.gradedFiniteEnvelopeScale 8 (sharpTailSquaredScale d) k * sharpTailEnvelope M omega) : ∃ (C : ℕ), SharpTailBounded M.gamma C omega

The joint envelope implies the sharp two-sided bounds with polynomial power one.

theorem Algsuperdiff.Section5.Field.ae_sharpTailGood {d : ℕ} (M : Section3.ABKModel d) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), SharpTailGood M.gamma omega

The sharp all-crossover shell event has full measure.