Closure

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

The unconditional lambda_{t,q} sensitivity provider

Source: ABK26, the lambda half of l.J.sensitivity.no.conditions.

This module discharges the single consumption point hdeep of Provider.Mesoscale.LambdaAssembly.unitCubeLambda_inv_le_of_mesoscale_descendant_ratio and assembles the provider form of the frozen target Algsuperdiff.Frozen.Section24.lambda_sensitivity_unconditional.

The mesoscopic depth kills the smallness gate

With X = C ‖∇h‖ λ_{s,2}^{-1}(□₀; a) and h = mesoscaleDepth s (1 + X), the scale-selection arithmetic of Provider.Mesoscale.ScaleSelection gives X · 3^{-(1-2s)h} ≤ 1. On a triadic descendant R of the unit cube at scale k ≤ -h, the sharp descendant scaling of the coarse gauge gives

|R| λ_{3/8,2}^{-1}(R; a) ≤ |R| λ_{s,2}^{-1}(R; a) ≤ 3^{(1-2s)k} λ_{s,2}^{-1}(□₀; a)
                        ≤ 3^{-(1-2s)h} λ_{s,2}^{-1}(□₀; a) ,

using 2s ≤ 1/2 < 3/4 for the first step (Book.Ch02.lambdaSq_mono). With C = 4 max{1, C_flux(d)} this is exactly the mesoscopic smallness condition 4 K_R λ_{3/8,2}^{-1}(R; a) ≤ 1/2 of the conditional per-cube estimate. No hypothesis on X is needed: when X is large the mesoscopic depth is large, and the depth is chosen so that the estimate closes for every X ≥ 0.

The sharp descendant scaling at the unit cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeScaleFactor_mul_lambdaSq_inv_le_rpow {d : ℕ} [NeZero d] (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs0 : 0 < s) (hq : q.IsAdmissible) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) : HCPolySupport.cubeScaleFactor R * (HCPolySupport.Book.Ch02.lambdaSq R s q F)⁻¹ ≤ Real.rpow 3 ((1 - 2 * s) * ↑k) * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d 0) s q F)⁻¹

The sharp descendant scaling of the coarse gauge at the unit cube. The scale-normalized gauge of a triadic descendant at scale k ≤ 0 gains exactly the factor 3^{(1-2s) k}. This is the display of ABK26.

The dimensional constant

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.unconditionalConst (d : ℕ) : ℝ

The constant of the frozen unconditional estimate: C = 4 max{1, C_flux(d)}, where C_flux(d) is the constant of the pure-flux D_h bound of Provider.Lambda.CubeBound.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.unconditionalConst d = 4 * max 1 (Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxCubeConst d)

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.unconditionalConst_pos (d : ℕ) : 0 < unconditionalConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.fluxCubeConst_le_max (d : ℕ) : Lambda.fluxCubeConst d ≤ max 1 (Lambda.fluxCubeConst d)

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.unitCubeLambda_inv_nonneg {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) : 0 ≤ (Frozen.Section24.unitCubeLambda s q a)⁻¹

The frozen coarse gauge is nonnegative.

Deep-cube smallness

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.deep_cube_smallness {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {s : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) {k : ℤ} (hkH : k ≤ (HCPolySupport.originCube d 0).scale - ↑(Mesoscale.mesoscaleDepth s (1 + unconditionalConst d * h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹))) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) : 4 * mesoFluxConst d h R * cubeGauge R a h.toLInfSkewMatrixFieldOn 0 ≤ 1 / 2

The smallness condition holds at every deep cube, unconditionally. At every triadic descendant of the unit cube of scale at most -h, with h the mesoscopic depth attached to the dimensionless parameter X = C ‖∇h‖ λ_{s,2}^{-1}(□₀; a), the dimensionless quantity governing the conditional per-cube estimate is at most 1/2.

This is the verification step of ABK26. No hypothesis on X is assumed: the mesoscopic depth grows with X exactly fast enough.

The provider

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.lambda_sensitivity_unconditional {d : ℕ} (dimension : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (s t : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent), 0 < s → s ≤ 1 / 4 → 0 < t → t ≤ 1 / 4 → q.IsAdmissible → (Frozen.Section24.unitCubeLambda t q (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1))⁻¹ ≤ 6 * (1 + C * h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹).rpow (2 * t / (1 - 2 * s)) * (Frozen.Section24.unitCubeLambda t q a)⁻¹

Unconditional sensitivity of lambda_{t,q}.

This is the provider form of the frozen target Algsuperdiff.Frozen.Section24.lambda_sensitivity_unconditional, with exactly the frozen binders: the full range 0 < s, t ≤ 1/4, every admissible q including the endpoint q = infinity, the literal constant 6, the exponent 2t/(1-2s), and no smallness gate.