ShellProductControl

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

The shell-corrector product of e.lower.bound.pre2

Step 5 of l.approximate.recurrence.formula needs

  limsup_K ( shom_{m-h}^{-2} E[ || h grad w_D^{(K)} ||^2_{L2(cu_K)} ]
             - E[ || grad w_D^{(K)} ||^2_{L2(cu_K)} ] )
    <= -(log 3) cstar shom_{m-h}^{-2} sum_{k=m-h+1}^m 3^{2 cgamma k}
       + C shom_{m-h}^{-4} h^2 3^{4 cgamma m} ,

"by e.perturb.assumption, e.km.kn.Lp, and Hoelder's inequality". The negative half is the fresh-shell corrector energy limit (lane shellsum-limit); the positive half is the product estimate proved here, whose two factors are

• the corrector moment E[|| grad w_D^{(K)} ||^4_{L4(cu_K)}]^{1/2}, controlled by e.nablaw.in.L.eight at C shom_{m-h}^{-2} h 3^{2 cgamma m}.

The scale bookkeeping --- that the two factors multiply to the printed shom^{-4} h^2 3^{4 cgamma m} --- is what this module proves, at the genuine Annealed.sigmaBar carrier and with the genuine rpow exponents. It is unconditional: the two moment bounds enter as numeric binders, named after their producers, and the Hoelder split itself enters as the numeric binder hprod.

References

• ABK26, e.lower.bound.pre2; the Hoelder step.
• ABK26, e.km.kn.Lp; e.nablaw.in.L.eight.
• ABK26, e.perturb.assumption.

The exponent bookkeeping

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.rpow_two_gamma_mul_self (gamma m : ℝ) : 3 ^ (2 * gamma * m) * 3 ^ (2 * gamma * m) = 3 ^ (4 * gamma * m)

The two shell factors 3^{2 cgamma m} multiply to the printed 3^{4 cgamma m}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sigmaBar_inv_sq_mul_self {d : ℕ} (M : ABKModel d) (n : ℤ) : (↑(Annealed.sigmaBar M n) ^ 2)⁻¹ * (↑(Annealed.sigmaBar M n) ^ 2)⁻¹ = (↑(Annealed.sigmaBar M n) ^ 4)⁻¹

The two gauge factors shom_n^{-2} multiply to the printed shom_n^{-4}.

The product control

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellProduct_le_quadratic_error {d : ℕ} (M : ABKModel d) {n : ℤ} {h : ℕ} {C1 C2 shellMoment gradMoment prod : ℝ} (hC1 : 0 ≤ C1) (hgrad0 : 0 ≤ gradMoment) (hprod : prod ≤ shellMoment * gradMoment) (hshell : shellMoment ≤ C1 * ↑h * 3 ^ (2 * M.gamma * ↑(n + ↑h))) (hgrad : gradMoment ≤ C2 * (↑(Annealed.sigmaBar M n) ^ 2)⁻¹ * ↑h * 3 ^ (2 * M.gamma * ↑(n + ↑h))) : (↑(Annealed.sigmaBar M n) ^ 2)⁻¹ * prod ≤ C1 * C2 * ↑h ^ 2 * (↑(Annealed.sigmaBar M n) ^ 4)⁻¹ * 3 ^ (4 * M.gamma * ↑(n + ↑h))

The Hoelder product, at the recurrence carriers.

shellMoment is E[|| k_{n+h} - k_n ||^4_{L4}]^{1/2} and gradMoment is E[|| grad w_D ||^4_{L4}]^{1/2}; hprod is the Cauchy--Schwarz/Hoelder split of shom_n^{-2} E[|| h grad w_D ||^2_{L2}], whose left factor this bounds.

The conclusion is exactly the quadratic h-error printed in the second line of e.what.do.we.have and carried by Closure.Step5GaugeEndpoint at Fend = * C2.

Binders, with their producers:

• hgrad --- e.nablaw.in.L.eight (at its own producer, not here);
• hprod --- the Hoelder split itself.

Unconditional.