LambdaSensitivityUnconditional

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

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

Unconditional sensitivity of lambda_{t,q}.