LambdaSensitivity

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

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

Conditional sensitivity of lambda_{s,q}.