LambdaAssembly

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

Assembly of the unconditional lambda sensitivity spine

This module assembles the mesoscopic scale selection (Mesoscale.ScaleSelection) with the mesoscale patching estimate (Mesoscale.Patching) and the root transfer of Multiscale.UnitCubeTransfer, producing the exact shape of the frozen lambda_sensitivity_unconditional conclusion (unitCubeLambda t q b)⁻¹ ≤ 6 * (1 + X)^{2t/(1-2s)} * (unitCubeLambda t q a)⁻¹

for 0 < s, t ≤ 1/4, every admissible q (including q = infinity) and every X ≥ 0, from a single consumption point: the per-cube ratio estimate with constant 2 on the triadic descendants of the unit cube at scales at most -h, where h = mesoscaleDepth s (1 + X).

The literal constant 6

6 = 2 * 3, where the 2 is the factor of the conditional lambda sensitivity estimate at a mesoscopic cube (its smallness parameter is at most 1 there by sub_one_mul_three_rpow_neg_mesoscaleDepth_le_one) and the 3 is three_rpow_two_mul_mesoscaleDepth_le. Neither the patching step nor the transfer step loses any constant, so the assembled constant is exactly 6.

Consumption points

• hdeep in unitCubeLambda_inv_le_of_mesoscale_descendant_ratio — the per-cube ratio estimate on descendant cubes.

Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers. The public unconditional statements will be obtained by discharging the consumption points, never by carrying them.

The assembled unconditional shape

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.unitCubeLambda_inv_le_of_mesoscale_descendant_ratio {d : ℕ} [NeZero d] (a b : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {s t X : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (ht0 : 0 < t) (ht : t ≤ 1 / 4) (hq : q.IsAdmissible) (hX : 0 ≤ X) (hdeep : ∀ (F G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d), (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a → (G.coeffOn (HCPolySupport.originCube d 0)).AEEq b → ∀ k ≤ (HCPolySupport.originCube d 0).scale - ↑(mesoscaleDepth s (1 + X)), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R G ≤ 2 * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R F) : (Frozen.Section24.unitCubeLambda t q b)⁻¹ ≤ 6 * (1 + X).rpow (2 * t / (1 - 2 * s)) * (Frozen.Section24.unitCubeLambda t q a)⁻¹

The unconditional lambda spine. From the per-cube ratio estimate with constant 2 on all triadic descendants of the unit cube at scales at most -h, with h = mesoscaleDepth s (1 + X), one obtains the exact frozen shape of lambda_sensitivity_unconditional, with the literal constant 6 and the exponent 2t/(1-2s), for every admissible q including q = infinity.