BigLambdaSensitivity

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

theorem Algsuperdiff.Frozen.Section24.bigLambda_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 : ℝ), 0 < s → s < 3 / 8 → unitCubeBigLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1) ≤ 4 * unitCubeBigLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a + C * (3 / 8 - s)⁻¹ * h.w1Infinity ^ 2 * (unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

Fixed-factor sensitivity of Lambda_{s,2}.