JResponseApplication

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

The good-carrier matrix estimate: the two deterministic legs of Step 1

This module supplies the two carrier-free ingredients of the J-response application of p.bfA.multiscalebound (ABK26):

2. the running-diffusivity comparison, sigmabar_{n-1} sigmabar_j^{-1} <=^{gamma(n-1-j)} and sigmabar_j sigmabar_{n-1}^{-1} <= C, with C = 4 explicit.

Local scope and downstream carrier transfer

The manuscript's Step 1 runs on a simplex spx of the Whitney simplex partition SW(square_n). This historical precursor does not itself construct that partition; both ingredients here are stated at the carrier-independent level at which the manuscript's argument uses them:

• the polarization split is proved for an arbitrary Ch02.Domain d — the bounded convex open carrier class of e.J.by.means.of.bfA, which contains cubes and simplices — so it applies without a new constant;
• the running-diffusivity comparison is a statement about sigmabar alone and carries no carrier.

The middle of Step 1 — the passage from J(spx, .; a_L) to Lambda_{1/4,2}(z + square_j; a_L) — begins in CrudeResponseBound.lean at the cube/descendant carrier. Thus the declarations below remain local providers, not a source-node closure.

The base case is not consumed

The node's dependency list names p.base.case, because it cites e.basecase.diffusivity "if `n

• 1 < mstar". In the frozen Lean rendering the citation is **redundant**: Algsuperdiff.Frozen.Section3.inductionState M m0 Etranscribes `d.mathcalS.defverbatim, ande.shom.h.boundsthere is asserted "for every `minZwithm <= m0" — with no lower bound. Both scales used, namely n
• 1andj = n - k - h_k <= n - 1, are below m0 = m - 1, so the two-sided sigmabarclause of the induction state alone proves both ratios. Consequently the frozendraft_sorry base_case` is not consumed, and no source-shaped A binder for it appears below.

Main results

• blockVecDot_coarseBlockMatrix_pure_potential, blockVecDot_coarseBlockMatrix_pure_flux: each pure leg of the block quadratic form is twice the corresponding response.
• blockVecDot_coarseBlockMatrix_le_four_responseJ_add: the polarization split, at an arbitrary domain.
• sigmaBar_le_four_mul_rpow_mul_sigmaBar, sigmaBar_le_four_mul_sigmaBar: the running-diffusivity comparison, with C = 4.

References

• ABK26 (p.bfA.multiscalebound, Step 1).
• ABK26, e.J.by.means.of.bfA.
• ABK26, d.mathcalS.def, e.shom.h.bounds.

The polarization split of e.J.by.means.of.bfA

theorem Algsuperdiff.Section3.Provider.Multiscale.blockVecDot_coarseBlockMatrix_pure_potential {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p : HCPolySupport.Vec d) : HCPolySupport.blockVecDot (p, 0) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) (p, 0)) = 2 * HCPolySupport.Book.Ch02.responseJ U a p 0

The pure-potential leg of e.J.by.means.of.bfA: on the load (p, 0) the bfA(U; a) quadratic form is 2 J(U, p, 0; a). The cross term - p . q is invisible at this loading.

theorem Algsuperdiff.Section3.Provider.Multiscale.blockVecDot_coarseBlockMatrix_pure_flux {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (q : HCPolySupport.Vec d) : HCPolySupport.blockVecDot (0, q) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) (0, q)) = 2 * HCPolySupport.Book.Ch02.responseJ U a 0 q

The pure-flux leg of e.J.by.means.of.bfA: on the load (0, q) the bfA(U; a) quadratic form is 2 J(U, 0, q; a).

theorem Algsuperdiff.Section3.Provider.Multiscale.blockVecDot_coarseBlockMatrix_le_four_responseJ_add {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (x y : HCPolySupport.Vec d) : HCPolySupport.blockVecDot (x, y) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) (x, y)) ≤ 4 * (HCPolySupport.Book.Ch02.responseJ U a x 0 + HCPolySupport.Book.Ch02.responseJ U a 0 y)

The polarization split of ABK26, at an arbitrary bounded convex domain. For every load (x, y) in R^{2d},

(x, y) . bfA(U; a) (x, y)  <=  4 ( J(U, x, 0; a) + J(U, 0, y; a) ) .

The manuscript writes the left side as |bfA^{1/2}(U; a) (x, y)|^2. The proof is the parallelogram identity together with the positive definiteness of bfA(U; a) on the residual load (x, -y); the two pure legs are then e.J.by.means.of.bfA.

Applied with (x, y) = bfAhom_{n-1}^{-1/2} P̂ = (sigmabar_{n-1}^{-1/2} p̂, sigmabar_{n-1}^{1/2} q̂), using that bfAhom is the block-diagonal diag(sigmabar, sigmabar^{-1}) of e.homs.defs, this is the manuscript's display verbatim.

The running-diffusivity comparison

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.sigmaEnvelope {d : ℕ} (M : ABKModel d) (m : ℤ) : ℝ

The induction-state envelope max{cstar gamma^{-1} 3^{2 gamma m}, nu^2}.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.sigmaEnvelope M m = max (Algsuperdiff.Section3.Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) (M.nu ^ 2)

theorem Algsuperdiff.Section3.Provider.Multiscale.sigmaBar_le_four_mul_rpow_mul_sigmaBar {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {i j : ℤ} (hji : j ≤ i) (hi : i ≤ m0) : ↑(Annealed.sigmaBar M i) ≤ 4 * 3 ^ (M.gamma * (↑i - ↑j)) * ↑(Annealed.sigmaBar M j)

The first running-diffusivity comparison of ABK26, with the constant C = 4 explicit:

sigmabar_i  <=  4 . 3^{gamma (i - j)} . sigmabar_j     for  j <= i <= m0 .

Only the two-sided clause e.shom.h.bounds of the induction state is used; see the module header on why p.base.case is not needed.

theorem Algsuperdiff.Section3.Provider.Multiscale.sigmaBar_le_four_mul_sigmaBar {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {i j : ℤ} (hji : j ≤ i) (hi : i ≤ m0) : ↑(Annealed.sigmaBar M j) ≤ 4 * ↑(Annealed.sigmaBar M i)

The second running-diffusivity comparison of ABK26, with the constant C = 4 explicit:

sigmabar_j  <=  4 sigmabar_i      for  j <= i <= m0 .