Spine

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

The conditional lambda_{s,q} sensitivity spine

Source: ABK26 (l.lambda.sensitivity).

This module assembles the ratio engine of Provider.Lambda.Engine with the self-referential bootstrap of Provider.Lambda.Bootstrap into the exact shape of the frozen conclusion

lambda_{s,q}^{-1}(a + h) ≤ (1 + C ‖∇h‖ lambda_{3/8,2}^{-1}(a)) lambda_{s,q}^{-1}(a)

for every s > 0 and every admissible q, from two inputs:

• hcube — the per-cube D_h bound at p = 0 on every triadic descendant of the unit cube, with the root gauge as coefficient;
• hcrude — any finite bound for the root gauge along the segment. The bootstrap uses it only to choose the mesh of the compounding grid; it does not enter the conclusion.

Both are premises of the internal helper below and must be discharged at every use. In particular the public provider result will carry neither.

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

The frozen gauge is an a.e. invariant

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.unitCubeLambda_pos {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 scalar unitCubeLambda is positive at every admissible exponent pair.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.unitCubeLambda_eq_of_aeeq {d : ℕ} (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) {a b : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))} (hab : a.AEEq b) : Frozen.Section24.unitCubeLambda s q a = Frozen.Section24.unitCubeLambda s q b

The frozen scalar unitCubeLambda only depends on the coefficient field up to a.e. equality.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.perturbCoeffOn_zero_aeeq {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) : (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h 0).AEEq a

The perturbation path starts at the base coefficient.

@[simp]

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.pathGauge_zero {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) : pathGauge a h 0 = (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

@[simp]

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.pathLambdaInv_zero {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) : pathLambdaInv a h s q 0 = (Frozen.Section24.unitCubeLambda s q a)⁻¹

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.pathLambdaInv_gauge {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) : pathLambdaInv a h (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) = pathGauge a h

The spine

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.unitCubeLambda_inv_perturb_le_of_cube_dhFluxForm_bound {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {K B : ℝ} (hK : 0 ≤ K) (hB : 0 ≤ B) (hcrude : ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → pathGauge a h t ≤ B) (hcube : ∀ (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d), (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) (τ : ℝ) (w : HCPolySupport.Vec d), |dhFluxForm (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) τ) (descendantField hk hR h) w| ≤ 2 * (K * pathGauge a h τ) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) τ) 0 w) (hsmall : 4 * K * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ 1 / 2) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) (hs : 0 < s) (hq : q.IsAdmissible) : (Frozen.Section24.unitCubeLambda s q (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h 1))⁻¹ ≤ (1 + 4 * K * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹) * (Frozen.Section24.unitCubeLambda s q a)⁻¹

The conditional lambda_{s,q} sensitivity, given the per-cube D_h bound.

hcube is the p = 0 specialization of the D_h bound applied on every triadic descendant of the unit cube and at every point of the segment, with the root coarse gauge as its coefficient. hcrude is any finite bound for the root gauge along the segment. Both are consumption points; neither appears in the final provider statement.