OffGridStabilityArith

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

The exponent and constant bookkeeping of the off-grid transport

The printed proof of l.lambdas.stability (ABK26) closes with a double geometric sum: an inner sum over the depths of the greedy family,

∑_{n ≤ k} 3^{-2sn} · C 3^{n-k}  =  C 3^{-2sk} / (1 - 3^{-(1-2s)}) ,

and an outer sum over the scales of the target quantity, which together produce the printed constant

C / (1 - 2s) · ( t / (t - s) )^{2/q} .

This module proves both sums and the constant, at q = 2 and in the exact Homogenization.geometricWeight normalization CoarseGraining's 𝓔_{·,∞,2} uses. It is pure real analysis: no cube, no coefficient field, no error functional appears.

The two elementary inequalities that drive everything

For y ∈ (0,1],

y / 2  ≤  1 - 3^{-y}  ≤  (3/2) y ,

the left from e^z ≥ 1 + z together with 1 ≤ log 3 (i.e. e < 3), the right from e^{-z} ≥ 1 - z together with log 3 ≤ 3/2 (i.e. 3 ≤ e^{3/2}). Both sides are needed: the lower bound converts the two geometric denominators into 2/(1-2u) and 1/(t-u), and the upper bound converts the numerator c_{2t} = 1 - 3^{-2t} into 3t, which is what turns the naive 1/(t-u) into the printed t/(t-u).

No nlinarith is used anywhere near an rpow/exp atom: every transcendental step is isolated in a named private lemma and consumed through linarith only [...].

The bookkeeping, end to end

With k the scale of the off-grid cube, K the scale of the enclosing grid cube, j = K - k, u the index of the parent cap and t the index asked of the off-grid cube (0 < u < t ≤ 1/2):

step	input	output
packing (geometry)	∑_{depth δ} |Q|/|V| ≤ 2d·3^{1-δ}	C = 6d
per-cube cap	J(Q) ≤ 3^{2u(K - scale Q)}·𝓔_u²	3^{2uj}·3^{2u(l+δ)}·𝓔_u²
inner sum	tsum_depth_le	12d/(1-2u)
outer sum	tsum_geometricWeight_two_mul_le	3t/(t-u)
product	offGridStabilityConst	36dt/((t-u)(1-2u))

At the printed slot (t,u) = (s/6, s/8) of e.mathcalE.stability.applied this is 36d·(s/6)/((s/24)(1 - s/4)) = 144 d/(1 - s/4) ≤ 192 d for s ≤ 1: a pure C(d), with no s-power deviation from the printed constant.

Main results

• half_le_one_sub_rpow_three_neg, one_sub_rpow_three_neg_le — the two-sided elementary bound.
• tsum_depth_le — the inner (greedy-family depth) sum.
• tsum_geometricWeight_two_mul_le — the outer (scale) sum.
• offGridStabilityConst, offGridStabilityConst_slot_le — the constant and its value at the printed slot.
• offGridStabilityError_bound — the shared nonnegative error-factor cap for any scale exponent at most one.

References

• ABK26, l.lambdas.stability, (both geometric sums).
• ABK26, e.mathcalE.stability.applied, (the slot).
• CoarseGraining, Homogenization/Book/Ch02/MultiscaleEllipticity.lean (geometricWeight, geometricDiscount).

0. Abstract-real helpers

Every step that would otherwise put a nonlinear tactic in sight of an exp, log or rpow atom is isolated here as a statement about abstract reals.

1. The two elementary bounds on 1 - 3^{-y}

theorem Algsuperdiff.Section4.Provider.ExcessDecay.one_le_log_three : 1 ≤ Real.log 3

e < 3, hence 1 ≤ log 3.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.log_three_le : Real.log 3 ≤ 3 / 2

3 ≤ e^{3/2}, hence log 3 ≤ 3/2.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.half_le_one_sub_rpow_three_neg {y : ℝ} (hy0 : 0 < y) (hy1 : y ≤ 1) : y / 2 ≤ 1 - 3 ^ (-y)

The lower bound. For y ∈ (0,1], y/2 ≤ 1 - 3^{-y}.

This is what converts the two geometric denominators of the printed proof into 2/(1-2s) and 1/(t-s).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.one_sub_rpow_three_neg_le {y : ℝ} (hy : 0 ≤ y) : 1 - 3 ^ (-y) ≤ 3 / 2 * y

The upper bound. For 0 ≤ y, 1 - 3^{-y} ≤ (3/2) y.

This is what turns the numerator c_{2t} = 1 - 3^{-2t} into 3t, hence the naive 1/(t-s) into the printed t/(t-s).

2. The geometric engine

theorem Algsuperdiff.Section4.Provider.ExcessDecay.summable_and_tsum_le_of_le_geometric {y C : ℝ} (hy0 : 0 < y) (hy1 : y ≤ 1) (hC : 0 ≤ C) (f : ℕ → ℝ) (hf0 : ∀ (n : ℕ), 0 ≤ f n) (hf : ∀ (n : ℕ), f n ≤ C * (3 ^ (-y)) ^ n) : Summable f ∧ ∑' (n : ℕ), f n ≤ 2 * C / y

The geometric engine. A nonnegative sequence dominated by C · (3^{-y})^n is summable with sum at most 2C/y.

3. The inner sum: the greedy-family depths

theorem Algsuperdiff.Section4.Provider.ExcessDecay.tsum_depth_le {u C : ℝ} (hu0 : 0 < u) (hu : u < 1 / 2) (hC : 0 ≤ C) (W : ℕ → ℝ) (hW0 : ∀ (n : ℕ), 0 ≤ W n) (hW : ∀ (n : ℕ), W n ≤ C * 3 ^ (-↑n)) : (Summable fun (n : ℕ) => W n * 3 ^ (2 * u * ↑n)) ∧ ∑' (n : ℕ), W n * 3 ^ (2 * u * ↑n) ≤ 2 * C / (1 - 2 * u)

The inner sum of the printed proof.

If the depth-δ weight of the greedy family is at most C·3^{-δ} — which is the covering geometry's packing count with C = 6d — then, after the per-cube cap has contributed its 3^{2uδ}, the depth sum is at most 2C/(1-2u).

This is ∑_{n ≤ k} 3^{-2un}·C·3^{n-k} ≤ C·3^{-2uk}·2/(1-2u) in the depth variable δ = k - n.

4. The outer sum: the scales of 𝓔_{·,∞,2}

theorem Algsuperdiff.Section4.Provider.ExcessDecay.tsum_geometricWeight_two_mul_le {t u A : ℝ} (hu0 : 0 < u) (hut : u < t) (ht : t ≤ 1 / 2) (hA : 0 ≤ A) (M : ℕ → ℝ) (hM0 : ∀ (l : ℕ), 0 ≤ M l) (hM : ∀ (l : ℕ), M l ≤ A * 3 ^ (2 * u * ↑l)) : (Summable fun (l : ℕ) => HCPolySupport.Book.Ch02.geometricWeight t 2 l * M l) ∧ ∑' (l : ℕ), HCPolySupport.Book.Ch02.geometricWeight t 2 l * M l ≤ 3 * t / (t - u) * A

The outer sum of the printed proof, in CoarseGraining's own weight normalization.

If the shell maxima M l of the off-grid cube obey M l ≤ A·3^{2ul} — which is what the inner sum delivers — then the 𝓔_{t,∞,2}-weighted series is at most 3t/(t-u)·A. The factor t in the numerator is the printed (t/(t-s))^{2/q} at q = 2; it comes from c_{2t} = 1 - 3^{-2t} ≤ 3t.

5. The composed constant

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.offGridStabilityConst (d : ℕ) (t u : ℝ) : ℝ

The constant of the off-grid transport at q = 2: 36 d t / ((t-u)(1-2u)), the product of the inner sum's 12d/(1-2u) and the outer sum's 3t/(t-u). Compare the printed C(d)(1-2s)^{-1}(t/(t-s))^{2/q}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.offGridStabilityConst d t u = 36 * ↑d * t / ((t - u) * (1 - 2 * u))

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridStabilityConst_nonneg {d : ℕ} {t u : ℝ} (hu0 : 0 < u) (hut : u < t) (ht : t ≤ 1 / 2) : 0 ≤ offGridStabilityConst d t u

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridStabilityConst_slot_le {d : ℕ} {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) : offGridStabilityConst d (s / 6) (s / 8) ≤ 192 * ↑d

The constant at the printed slot (t,u) = (s/6, s/8) of e.mathcalE.stability.applied: a pure C(d), with no s-power deviation. For s ∈ (0,1] it is at most 192 d.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridStabilityError_bound {d : ℕ} {s exponent E : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hexponent : exponent ≤ 1) (hE : 0 ≤ E) : 0 ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ exponent * E) ∧ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ exponent * E) ≤ √(192 * ↑d) * 3 * E

The off-grid error factor is bounded uniformly when its scale exponent is at most one.