ResponseJSensitivity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
theorem
Algsuperdiff.Frozen.Section24.responseJ_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 →
∀ (p q : HCPolySupport.Vec d) (δ : ℝ),
0 < δ →
δ ≤ 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)
p q ≤ (1 + δ + C * h.gradientW1Infinity * (unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹) * HCPolySupport.Book.Ch02.responseJ
(HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q + C * δ⁻¹ * (HCPolySupport.vecNormSq p * h.w1Infinity ^ 2 * (unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ + |HCPolySupport.vecDot p q| * h.gradientW1Infinity ^ 2 * (unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ^ 2)
Conditional sensitivity of the response functional.