CubeJSensitivity

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

The descendant b-matrix estimate

Source: ABK26, the display

|b(z + cu_n; a + h)| ≤ 4 |b(z + cu_n; a)| + C ‖h‖²_{W^{1,∞}(cu_0)}
                          λ_{3/8,2}^{-1}(z + cu_n; a) ,

obtained by applying the J-sensitivity estimate on each descendant cube with the scaled-norm inequalities of that display.

The route here is:

1. the pure-potential D_h bound of BigLambda.CubePotentialDh, transported along the perturbation path and priced against the base descendant gauge and the base root gauge (BigLambda.CubeGaugePath);
2. the frozen derivative identity Provider.Response.PathDerivative turns it into the affine differential inequality y' ≤ m + c y after a pointwise Young step (BigLambda.PathODE);
3. exact integration of that inequality gives the J-sensitivity at the pure-potential loading, uniformly in the descendant;
4. the identity 2 J(R, p, 0; a) = p · b(R; a) p of BigLambda.BMatrix converts it into the descendant b-matrix estimate, with the same-index factor 4 and a cube-independent constant K = C(d) ‖h‖²_{W^{1,∞}}.

Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers.

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambdaGateConst (d : ℕ) : ℝ

A common threshold constant for gauge and potential sensitivity estimates.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambdaGateConst_pos (d : ℕ) : 0 < bigLambdaGateConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.gaugeGateConst_le_bigLambdaGateConst (d : ℕ) : gaugeGateConst d ≤ bigLambdaGateConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.four_mul_potCubeConstB_le_bigLambdaGateConst (d : ℕ) : 4 * potCubeConstB d ≤ bigLambdaGateConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.gaugeGate_of_bigLambdaGate {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (bigLambdaGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) : h.gradientW1Infinity ≤ (gaugeGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a

The pure-potential D_h bound along the path

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.abs_dhPotentialForm_le_base_gauges {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (bigLambdaGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) (F : HCPolySupport.Book.Ch03.CoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) {τ : ℝ} (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1) (p : HCPolySupport.Vec d) : |dhPotentialForm (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Lambda.descendantField hk hR h.toLInfSkewMatrixFieldOn) τ) (Lambda.descendantField hk hR h.toLInfSkewMatrixFieldOn) p| ≤ potCubeConstA d * √2 * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p * (√(HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Lambda.descendantField hk hR h.toLInfSkewMatrixFieldOn) τ) p 0)) + potCubeConstB d * h.gradientW1Infinity * (2 * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Lambda.descendantField hk hR h.toLInfSkewMatrixFieldOn) τ) p 0

The pure-potential D_h bound at a descendant, priced against the base gauges. The Term A factor uses the descendant gauge at the base point; the Term BC factor uses the root gauge at the base point.

The per-cube J-sensitivity at the pure-potential loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.responseJ_potential_cube_sensitivity {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (bigLambdaGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) (F : HCPolySupport.Book.Ch03.CoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (p : HCPolySupport.Vec d) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Lambda.descendantField hk hR h.toLInfSkewMatrixFieldOn) 1) p 0 ≤ (1 + δ / 2 + 2 * (potCubeConstB d * h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹)) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) p 0 + δ⁻¹ * (potCubeConstA d ^ 2 * h.w1Infinity ^ 2 * HCPolySupport.vecNormSq p * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹)

The pure-potential J-sensitivity on a descendant cube.

The δ-range is the frozen one, 0 < δ ≤ 1; the energy term carries the descendant gauge, exactly as in the source display.