Arithmetic

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

Arithmetic for the small-contrast Schauder iteration

This file isolates the numerical part of the small-contrast iteration. In particular, it retains the author's constants 2^(-3-d/2), 1/8, and 2^(d/2) literally, so the analytic modules do not hide any dependence on the Hölder exponent in a generic constant.

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold (d : ℕ) (alpha : ℝ) : ℝ

The coefficient-oscillation threshold in the small-contrast estimate.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold d alpha = 2 ^ (-(3 + ↑d / 2)) * (1 - alpha)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.one_add_quarter_mul_le_one_sub_eighth_mul_two_rpow {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : 1 + x / 4 ≤ (1 - x / 8) * 2 ^ x

The elementary numerical inequality used to select the contraction parameter at theta = 1/2.

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastContraction (alpha : ℝ) : ℝ

The contraction factor in the printed dyadic iteration.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastContraction alpha = 1 - (1 - alpha) / 8

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastContraction_mem_Ioo {alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) : smallContrastContraction alpha ∈ Set.Ioo 0 1

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.one_sub_smallContrastContraction (alpha : ℝ) : 1 - smallContrastContraction alpha = (1 - alpha) / 8

The reciprocal contraction gap is the displayed (1-alpha)⁻¹ price.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.two_mul_smallContrastThreshold_mul_half_rpow (d : ℕ) (alpha : ℝ) : 2 * smallContrastThreshold d alpha * (1 / 2) ^ (-↑d / 2) = (1 - alpha) / 4

At theta = 1/2, the perturbative coefficient produced by the printed threshold is exactly (1-alpha)/4. This is the cancellation of the displayed 2^(-d/2) and 2^(d/2) factors.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold_nonneg (d : ℕ) {alpha : ℝ} (halpha : alpha ≤ 1) : 0 ≤ smallContrastThreshold d alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold_le_eighth_gap (d : ℕ) {alpha : ℝ} (halpha : alpha ≤ 1) : smallContrastThreshold d alpha ≤ (1 - alpha) / 8

The printed threshold is in particular at most (1-alpha)/8.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold_lt_half (d : ℕ) {alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) : smallContrastThreshold d alpha < 1 / 2

The corrected coercivity step only needs delta < 1/2; the printed threshold has much more room.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.dyadic_smallContrast_contraction {d : ℕ} {alpha delta : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) (hdelta : delta ≤ smallContrastThreshold d alpha) : (1 + 2 * delta * (1 / 2) ^ (-↑d / 2)) * (1 / 2) ^ (1 - alpha) ≤ smallContrastContraction alpha

The exact theta = 1/2 contraction in the source. No constant in this statement depends on alpha: all exponent dependence is visible through 1-alpha.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.inv_one_sub_smallContrastContraction_le {alpha : ℝ} (halpha : alpha < 1) : (1 - smallContrastContraction alpha)⁻¹ ≤ 8 * (1 - alpha)⁻¹

At the printed contraction, summing the recurrence costs exactly at most 8 * (1-alpha)⁻¹.