HomLiftScaleArith

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

Theorem B, §4.5, Step 3c: the triadic scale arithmetic of the Hölder

lifting

This module isolates the three purely arithmetic ingredients of the Step-3c bridge

  3^{-m} ‖u - v‖_{L^∞(□_m)} ≤ C 3^{-ms} ‖∇u - ∇v‖_{W_hat^{-s,∞}(□_m)},

read through the (∞,∞)-index Hölder lifting: a negative-order bound on ∇w at exponent -s lifts to the C^{0,1-s} seminorm of w, which is stronger than L^∞. The three ingredients are

• exists_triadic_scale — for 0 < t ≤ 3^m there is a triadic scale n ≤ m with 3^n ≤ t < 3^{n+1}. This is the scale at which the telescoping argument is cut.
• liftGeomFactor s = (1 - 3^{-(1-s)})⁻¹ — the geometric factor of the telescoping sum over the scales below n, together with the bound liftGeomFactor s ≤ 3 valid on the whole range 0 < s ≤ 1/2.
• three_rpow_le_two — 3^s ≤ 2 on 0 ≤ s ≤ 1/2, the factor lost when the Lipschitz term of the regularization is converted into a t^{1-s} term.

The s-dependence. Both constants are bounded uniformly on s ∈ (0,1/2]; neither carries a (1-s)^{-1} factor there. The blow-up of liftGeomFactor is at the endpoint s → 1, which this development never approaches: the §4.5 parameter selection pins s = |log γ|⁻¹, and Step 3 additionally records s < 1/10 for small γ. So the lifting's constant is absolutely bounded at the pin and nothing has to be absorbed by the E_{ThmB}(m) budget.

References

• ABK26, Theorem B Step 3 (the bridge display).
• ABK26 (the introduction's W^{-s,∞} ↔ Hölder remark) and ([·]_{C^{0,s}} vs [·]_{W^{s,∞}}).

1. Powers of three: zpow versus rpow

theorem Algsuperdiff.Section4.Provider.Homogenization.natCast_three : ↑3 = 3

The base 3 used by Int.log is the natural-number literal; this is its identification with the real literal.

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_intCast (n : ℤ) : 3 ^ ↑n = ↑3 ^ n

A real power of 3 at an integer exponent is the corresponding zpow.

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_pos (t : ℝ) : 0 < 3 ^ t

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_nonneg (t : ℝ) : 0 ≤ 3 ^ t

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_le_three_rpow {a b : ℝ} (hab : a ≤ b) : 3 ^ a ≤ 3 ^ b

Real powers of 3 are monotone in the exponent.

2. Triadic scale selection

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_triadic_scale {t : ℝ} (ht : 0 < t) {m : ℤ} (htm : t ≤ 3 ^ ↑m) : ∃ n ≤ m, 3 ^ ↑n ≤ t ∧ t < 3 ^ ↑(n + 1)

The scale cut. For 0 < t ≤ 3^m there is a triadic scale n ≤ m with 3^n ≤ t < 3^{n+1}.

This is the scale at which the telescoping Hölder argument is cut: below n one uses the approximation estimate, at n the Lipschitz estimate.

3. The two absolute constants

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_half_ge : 3 / 2 ≤ 3 ^ (1 / 2)

3^{1/2} ≥ 3/2.

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_half_le_two : 3 ^ (1 / 2) ≤ 2

3^{1/2} ≤ 2.

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_le_two {s : ℝ} (hs : s ≤ 1 / 2) : 3 ^ s ≤ 2

3^s ≤ 2 on 0 ≤ s ≤ 1/2 — the factor lost when the Lipschitz term of the scale-n regularization is converted into a t^{1-s} term.

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.liftGeomFactor (s : ℝ) : ℝ

The telescoping geometric factor (1 - 3^{-(1-s)})⁻¹, the sum of the geometric series ∑_{k≥0} 3^{-k(1-s)} governing the increments of the regularization family below a given scale.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.liftGeomFactor s = (1 - 3 ^ (-(1 - s)))⁻¹

theorem Algsuperdiff.Section4.Provider.Homogenization.liftGeomFactor_def (s : ℝ) : liftGeomFactor s = (1 - 3 ^ (-(1 - s)))⁻¹

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_neg_one_sub_le {s : ℝ} (hs : s ≤ 1 / 2) : 3 ^ (-(1 - s)) ≤ 2 / 3

On s ≤ 1/2 the geometric ratio is at most 2/3.

theorem Algsuperdiff.Section4.Provider.Homogenization.one_sub_three_rpow_pos {s : ℝ} (hs : s < 1) : 0 < 1 - 3 ^ (-(1 - s))

theorem Algsuperdiff.Section4.Provider.Homogenization.liftGeomFactor_pos {s : ℝ} (hs : s < 1) : 0 < liftGeomFactor s

theorem Algsuperdiff.Section4.Provider.Homogenization.liftGeomFactor_nonneg {s : ℝ} (hs : s < 1) : 0 ≤ liftGeomFactor s

theorem Algsuperdiff.Section4.Provider.Homogenization.liftGeomFactor_le_three {s : ℝ} (hs : s ≤ 1 / 2) : liftGeomFactor s ≤ 3

The s-dependence of the lifting. On the whole range s ≤ 1/2 — in particular at the §4.5 pin s = |log γ|⁻¹, and a fortiori under Step 3's own s < 1/10 — the telescoping factor is bounded by the absolute constant 3. No (1-s)^{-1} factor is incurred.

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_sub_natCast_mul (a c : ℝ) (j : ℕ) : 3 ^ ((a - ↑j) * c) = 3 ^ (a * c) * (3 ^ (-c)) ^ j

Descending j triadic scales multiplies the weight 3^{ac} by the j-th power of the geometric ratio 3^{-c}. This is the identity that turns the scale-indexed increment estimate into a geometric series.

4. Geometric sums

theorem Algsuperdiff.Section4.Provider.Homogenization.geom_sum_three_rpow_le {s : ℝ} (hs : s < 1) (k : ℕ) : ∑ i ∈ Finset.range k, (3 ^ (-(1 - s))) ^ i ≤ liftGeomFactor s

The finite geometric sums of the ratio 3^{-(1-s)} are bounded by liftGeomFactor s.