PrincipalResponseCentre

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

Provider: the centering estimate for the fresh shell on the localization cube

Source displays in ABK26:

• the fresh shell h := k_m - k_{m-h} named;
• Step 3 of l.approximate.recurrence.formula (label), whose Young remainder is absorbed using ||h - (h)_{z+cu_n}||^2 <= Delta^2 shom_{m-h} lambda_{3/8,2};
• the gauge 3^{2n} ||grad (k_m - k_{m-h})||_{W^{1,infinity}(z+cu_n)} of e.good.local.events (label; display), carried in this repository as Provider.BadEvents.incrementOscGauge₂.

What this module supplies

ApproximateRecurrence.PrincipalResponseSwitchActualShellSize reduces the shell-size hypothesis of the per-cube switch to the single inequality

hcentre :  ||h - (h)_{z+cu_n}||_{W^{1,infinity}}  <=  K . osc ,

which it carries as a binder with K free. This module supplies that inequality, with the explicit K = d^3 recorded in centeringConst, and then supplies the shell-size hypothesis with that binder discharged.

The estimate is elementary and is not an L^2 Poincare inequality. Three elementary bridges are involved.

1. Essential supremum from a pointwise bound. The frozen UnitCubeSkewW2Infinity.w1Infinity reads both of its fields through eLpNorm ... ∞ on the literal open unit cube, so a bound holding at every point of that cube bounds it; this is w1Infinity_shellFieldUnitCube_le. Its gradient component is below the manuscript gauge with constant one, by the proved normalization Provider.BadEvents.max_unitCubeDerivNorm_cube, because a constant shift is invisible to cubeOscGauge.

2. Mean value on the localization cube. A shell field is C^2 and carries its own derivative, so Mathlib's mean value inequality applies verbatim on the convex open cube, whose sup-norm diameter is the side length 3^n. Averaging the resulting bound over the cube against the constant h(x) gives the centering bound entrywise, and the entrywise bound is converted to the Euclidean matrix norm by the proved comparisons of Section24.Sensitivity.Provider.DhBound.Lipschitz.MatrixNorms.

3. Rescaling. The manuscript's (h)_{z+cu_n} is ApproximateRecurrence.freshShellCubeAverage, an average of the unrescaled shell over cubeSet R, whereas the centered object lives at the rescaled unit cube. The route taken here runs the mean value argument at the unrescaled cube R and transports the gradient bound through Provider.BadEvents.max_unitCubeDerivNorm_cube and the chain rule of ShellField.spatialScale; no change-of-variables formula for the cube average is used.

The constant

centeringConst d = d^3. One factor d comes from the comparison between the ambient sup norm of Vec d and the frozen derivative norm (norm_le_sum_basisVec_apply over the d coordinate directions), and the remaining d^2 from matrixNorm_le_sq_mul_norm. The constant enters the consumer only through shellSizeThreshold M Ccg (centeringConst d) lowScale, whose comparison with S remains a binder about the data of the recurrence.

Carriers

• the localization cube is a free TriadicCube d; no literal buffer constant of e.recurrence.params occurs;
• the two scales are free integers lowScale <= highScale;
• cstar does not occur in this module.

Main definitions

• centeringConst: the explicit constant d^3 of the centering estimate.

Main results

• w1Infinity_centeredShellUnitCube_le: the centering estimate for the shell centered at any constant that is its own cube average.
• w1Infinity_centeredFreshShellUnitCube_le: the same at the manuscript's own constant (h)_{z+cu_n}.
• shell_hypothesis_of_centeringConst_ae: the shell-size hypothesis the per-cube switch consumes, obtained from shell_hypothesis_of_centering_ae at K = centeringConst d with its centering binder discharged.

Elementary comparisons between the entrywise and Euclidean matrix norms

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.norm_mat_le_matrixNorm {d : ℕ} (A : HCPolySupport.Mat d) : ‖A‖ ≤ HCPolySupport.Book.Ch02.matrixNorm A

The ambient entrywise supremum norm of a matrix is below its Euclidean matrix norm.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.norm_clm_le_card_mul_matrixDerivativeNorm {d : ℕ} (D : Frozen.Assumptions.ShellField.MatrixDerivative d) : ‖D‖ ≤ ↑d * Frozen.Assumptions.ShellField.matrixDerivativeNorm D

The ambient operator norm of a matrix-valued derivative, from the sup norm of Vec d to the entrywise norm of Mat d, is below d times the exact induced derivative norm.

The literal open cubes as metric balls

Averaging against a value taken on the open cube

Regularity of the entries of a shell field

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.matEntryCLM {d : ℕ} (i j : Fin d) : HCPolySupport.Mat d →L[ℝ] ℝ

Extract a matrix entry as a continuous linear functional for the recurrence estimate.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.matEntryCLM i j = { toFun := fun (A : HCPolySupport.Mat d) => A i j, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Bridge (i): a pointwise bound on the open unit cube

The rescaled shell field at a triadic cube

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.rescaledField {d : ℕ} (R : HCPolySupport.TriadicCube d) (g : Frozen.Assumptions.ShellField d) : Frozen.Assumptions.ShellField d

The shell field on z + square_j transported to the unit cube by the manuscript's map y |-> z + 3^j y.

Equations

• One or more equations did not get rendered due to their size.

The constant

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.centeringConst (d : ℕ) : ℝ

The explicit constant of the centering estimate: d^3. One factor d comes from the comparison between the ambient sup norm of Vec d and the exact induced derivative norm, and the remaining d^2 from matrixNorm_le_sq_mul_norm.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.centeringConst d = ↑d ^ 3

Bridges (ii) and (iii): the centering estimate

The consumer: the shell-size hypothesis with hcentre supplied

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shell_hypothesis_of_centeringConst_ae {d : ℕ} [NeZero d] (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) (j : ℕ) {lowScale highScale : ℤ} (hle : lowScale ≤ highScale) {S : ℝ} (hS : shellSizeThreshold M Ccg (centeringConst d) lowScale ≤ S) (R : HCPolySupport.TriadicCube d) : R ∈ HCPolySupport.descendantsAtDepth Q j → ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), omega ∈ BadEvents.goodLocalEvent M Ccg R lowScale → (centeredFreshShellUnitCube M R hle omega).w1Infinity ^ 2 ≤ gridSwitchDiscount Q j lowScale ^ 2 * S * HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M lowScale omega)

The binder hshell of the per-cube switch, with the centering estimate supplied.

This is ApproximateRecurrence.shell_hypothesis_of_centering_ae at K = centeringConst d, with its binder hcentre discharged by w1Infinity_centeredFreshShellUnitCube_le.

: this statement holds only under the propositions supplied by its binders -- hCcg (0 < Ccg), hle (m - h <= m) and hS, the threshold comparison shellSizeThreshold M Ccg (centeringConst d) lowScale <= S, which is a condition on the data of the recurrence -- together with the membership in the good event carried inside the almost-sure conclusion. It is a provider A, not a source-facing frozen declaration.