ResponseJSensitivityUnconditional

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

theorem Algsuperdiff.Frozen.Section24.responseJ_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 μ σ0 : ℝ) (e : HCPolySupport.Vec d), 0 < s → s ≤ 1 / 4 → 0 < t → t ≤ 1 / 4 → 0 < μ → 0 < σ0 → HCPolySupport.Book.Ch02.vecNorm e = 1 → HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1) ((√(μ * σ0))⁻¹ • e) (√(μ * σ0) • e) ≤ C * μ⁻¹ * (1 + h.gradientW1Infinity * (unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹).rpow (2 * t / (1 - 2 * s)) * unitCubeHomogenizationError t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a (HCPolySupport.scalarMatrix σ0) ^ 2 + C * μ⁻¹ * σ0 * (unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * (1 + h.gradientW1Infinity * (unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹).rpow (2 * s / (1 - 2 * s)) * (σ0⁻¹ ^ 2 * h.valueL2 ^ 2 + (μ - 1) ^ 2) + C * μ⁻¹ ^ 2 * σ0⁻¹ ^ 2 * h.gradientW1Infinity ^ 2 + C * min 1 (h.gradientW1Infinity * (unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹) ^ 2

Unconditional four-term sensitivity estimate for the response functional.