UniformExhaustionBudget

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

Uniform exhaustion budgets

The shift-uniform profile has a finite cubic layer-cake budget. Its cubic-log cutoff also has an explicit subpolynomial growth bound for exponents strictly between one and two.

noncomputable def Algsuperdiff.Section5.Field.streamUniformExhaustionBudget {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : ℝ

The uniform cubic layer-cake budget.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.streamUniformExhaustionGrowth {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (q : ℝ) : ℝ

The explicit constant in the subpolynomial cutoff-growth estimate.

Equations

• Algsuperdiff.Section5.Field.streamUniformExhaustionGrowth M omega q = if 1 < q ∧ q < 2 then Algsuperdiff.Section5.Field.streamUniformExhaustionScale M omega ^ 12 * (1 + 12 / (2 - q)) ^ 12 else 0

theorem Algsuperdiff.Section5.Field.streamUniformExhaustionBudget_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : 0 ≤ streamUniformExhaustionBudget M omega

The displayed uniform budget is nonnegative.

theorem Algsuperdiff.Section5.Field.lintegral_streamUniformExhaustionProfile_mul_cube_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {lam : ℝ} (hlam : 1 ≤ lam) : ∫⁻ (s : ℝ) in Set.Ioi (streamUniformExhaustionCutoff M omega lam), ENNReal.ofReal (streamUniformExhaustionProfile M omega lam s * s ^ 3) ≤ ENNReal.ofReal (streamUniformExhaustionBudget M omega)

Above the cutting radius, the cubic layer-cake integral is bounded by the shift-independent displayed budget.

theorem Algsuperdiff.Section5.Field.streamUniformExhaustionGrowth_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {q : ℝ} (hq1 : 1 < q) (hq2 : q < 2) : 0 ≤ streamUniformExhaustionGrowth M omega q

The cutoff-growth coefficient is nonnegative in the admissible exponent range.

theorem Algsuperdiff.Section5.Field.streamUniformExhaustionCutoff_pow_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {q : ℝ} (hq1 : 1 < q) (hq2 : q < 2) {lam : ℝ} (hlam : 1 ≤ lam) : streamUniformExhaustionCutoff M omega lam ^ 4 ≤ streamUniformExhaustionGrowth M omega q * lam ^ (2 - q)

The fourth power of the cubic-log cutoff is subpolynomial in the shift, with an explicit coefficient for every fixed exponent q ∈ (1,2).