CaccioppoliInteriorPrefactor

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

Discharging the Caccioppoli prefactor from the good-event ellipticity caps

CoarseGraining's coarse Caccioppoli with right-hand side carries the prefactor

  (C/σ)^{2 + 4s/σ} · s^{-2s/σ} · Θ_{s,t}^{(1-t)/σ} ,      σ = 1 - s - t ,

with Θ_{s,t} = Λ_{s,1}/λ_{t,1} — the q = 1 coarse-grained ellipticity constants. The proved good-event caps (GoodEventCaps.lean, SlotTransportChildCube.lean) bound the q = 2 ratios. This module supplies the two missing pieces:

1. the q = 1 ← q = 2 comparison for Λ and λ⁻¹ (§1). The weights of the two definitions coincide, w_{u,1} = w_{u/2,2}, and CoarseGraining's own Jensen split then gives

     Λ_{u,1} ≤ Λ_{u/2,2} ,      λ_{u,1}^{-1} ≤ λ_{u/2,2}^{-1}
   

   with no constant.
2. the parameter choice that makes the prefactor a dimensional constant (§2--§3). The Caccioppoli's first exponent is a free parameter of the lemma; taking it to be the absolute constant 1/4 and the second to be t = s/4 gives, for every s ∈ (0,1],

     σ = 3/4 - s/4 ∈ [1/2, 3/4) ,   2 + 4·(1/4)/σ ≤ 4 ,
     (1/4)^{-2·(1/4)/σ} ≤ 4 ,       (1-t)/σ ≤ 2 ,
   

   so the prefactor is at most (2 max(1,C))^4 · 4 · Θ_0^2 — no transcendental estimate is needed anywhere, and the whole s-dependence of the estimate is pushed into the forcing factor t^{-8}(1-2t)^{-1} ≤ 131072 s^{-8} (§3).

The index choice is exactly what the caps admit: the q = 1 ← q = 2 step at index u needs the q = 2 cap at u/2, and the caps hold for every q = 2 index ≥ s/8; here u = 1/4 gives 1/8 ≥ s/8 (as s ≤ 1) and u = s/4 gives exactly s/8.

Deviation from print, recorded

The specialization chosen here is (1/4, s/4); it yields the squared forcing envelope s^{-8}, i.e. s^{-4} on the un-squared display, which is stronger than the printed s^{-11/2} on 0 < s ≤ 1 (s^{-8} ≤ s^{-11} squared). Both forms are delivered: the honest s^{-8} and, by weakening, the printed s^{-11}.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS; e.energy.bound.interior; e.compareEqs.
• CoarseGraining, Ch02.LambdaSq_finite_one_le_tsum_weighted_maxDescendantBMatrixNormAtScale, Ch02.lambdaSq_finite_one_inv_le_tsum_weighted_maxDescendantSigmaStarInvMatrixNormAtScale, Ch02.LambdaSqFinite_rpow_q_div_two_eq_tsum, Ch02.one_le_ThetaRatio_of_pos.

1. The q = 1 ← q = 2 comparison for the ellipticity constants

theorem Algsuperdiff.Section4.Provider.ExcessDecay.LambdaSq_finite_two_eq_tsum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {u : ℝ} (hu : 0 < u) : HCPolySupport.Book.Ch02.LambdaSq Q u (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a = ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight u 2 n * HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a

Λ_{u,2} is the weighted shell series of the operator norms.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.lambdaSq_finite_two_inv_eq_tsum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {u : ℝ} (hu : 0 < u) : (HCPolySupport.Book.Ch02.lambdaSq Q u (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ = ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight u 2 n * HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a

λ_{u,2}⁻¹ is the weighted shell series of the inverse lower norms.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.LambdaSq_finite_one_le_finite_two_half {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {u : ℝ} (hu : 0 < u) : HCPolySupport.Book.Ch02.LambdaSq Q u (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) a ≤ HCPolySupport.Book.Ch02.LambdaSq Q (u / 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a

The q = 1 ← q = 2 comparison for the upper constant.

  Λ_{u,1}(Q; a) ≤ Λ_{u/2,2}(Q; a)

with no constant: the two weight families coincide and CoarseGraining's Jensen split turns the q = 1 square root into the q = 2 linear series.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.lambdaSq_finite_one_inv_le_finite_two_half {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {u : ℝ} (hu : 0 < u) : (HCPolySupport.Book.Ch02.lambdaSq Q u (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) a)⁻¹ ≤ (HCPolySupport.Book.Ch02.lambdaSq Q (u / 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

The q = 1 ← q = 2 comparison for the inverse lower constant.

  λ_{u,1}(Q; a)⁻¹ ≤ λ_{u/2,2}(Q; a)⁻¹ .

2. From the q = 2 ratio cap to the q = 1 ingredients

theorem Algsuperdiff.Section4.Provider.ExcessDecay.LambdaS_le_of_ratio_cap {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {u sigma K : ℝ} (hu : 0 < u) (hsigma : 0 < sigma) (hcap : sigma⁻¹ * HCPolySupport.Book.Ch02.LambdaSq Q (u / 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a ≤ K) : HCPolySupport.Book.Ch02.LambdaS Q u a ≤ K * sigma

The upper q = 1 cap. A q = 2 ratio cap at index u/2 caps the q = 1 upper constant at index u.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.lambdaS_inv_le_of_ratio_cap {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {u sigma K : ℝ} (hu : 0 < u) (hsigma : 0 < sigma) (hcap : sigma * (HCPolySupport.Book.Ch02.lambdaSq Q (u / 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ K) : (HCPolySupport.Book.Ch02.lambdaS Q u a)⁻¹ ≤ K * sigma⁻¹

The lower q = 1 cap. A q = 2 ratio cap at index u/2 caps the inverse q = 1 lower constant at index u.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.lambdaS_le_LambdaS {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) : HCPolySupport.Book.Ch02.lambdaS Q t a ≤ HCPolySupport.Book.Ch02.LambdaS Q s a

The lower constant is dominated by the upper one at any two positive indices (CoarseGraining's one_le_ThetaRatio_of_pos, read as an inequality).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.thetaRatio_le_of_caps {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s t B1 B2 : ℝ} (hs : 0 < s) (ht : 0 < t) (hB1 : HCPolySupport.Book.Ch02.LambdaS Q s a ≤ B1) (hB2 : (HCPolySupport.Book.Ch02.lambdaS Q t a)⁻¹ ≤ B2) : HCPolySupport.Book.Ch02.ThetaRatio Q s t a ≤ B1 * B2

The contrast Θ is capped by the product of the two q = 1 caps.

3. The prefactor and the forcing factor at the chosen parameters

theorem Algsuperdiff.Section4.Provider.ExcessDecay.caccioppoliWithRHSPrefactor_quarter_le {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {C s Theta0 : ℝ} (hC : 0 < C) (hs : 0 < s) (hs1 : s ≤ 1) (hTheta : HCPolySupport.Book.Ch02.ThetaRatio Q (1 / 4) (s / 4) a ≤ Theta0) : HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C Q a (1 / 4) (s / 4) ≤ (2 * max 1 C) ^ 4 * 4 * Theta0 ^ 2

The prefactor at (s_c, t_c) = (1/4, s/4) is a constant.

For every s ∈ (0,1], every C ≥ 1 and every cap Θ ≤ Θ₀,

  (C/σ)^{2+4·(1/4)/σ} · (1/4)^{-2·(1/4)/σ} · Θ^{(1-s/4)/σ} ≤ (2C)^4 · 4 · Θ₀² ,

σ = 1 - 1/4 - s/4 ∈ [1/2, 3/4). Every step is a rational comparison of rpow exponents; no transcendental estimate is used.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.forcing_factor_quarter_le {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : (s / 4).rpow (-8) / (1 - 2 * (s / 4)) ≤ 131072 * s.rpow (-8)

The forcing factor. At t = s/4 with s ∈ (0,1],

  t^{-8} (1 - 2t)^{-1} ≤ 131072 · s^{-8} .