Closure

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

The unconditional response estimate, modulo the per-mesoscopic-cube input

Source: ABK26, the J half of l.J.sensitivity.no.conditions.

The result

responseJ_sensitivity_unconditional_of_mesoscale_cube_sensitivity

has exactly the frozen conclusion of Algsuperdiff.Frozen.Section24.responseJ_sensitivity_unconditional, including the letI : NeZero d, and exactly one hypothesis, hcube, which is the missing analytic input in its precise form.

What hcube says

There are dimensional constants C₀ ≥ 1 and K₁ ≥ 0 such that, at the mesoscopic depth H = mesoscaleDepth s (1 + C₀ ‖∇h‖ λ_{s,2}^{-1}(□₀;a)), on every triadic cube R of depth H below the unit cube,

J(R, a+h, (μσ₀)^{-1/2}e, (μσ₀)^{1/2}e)
  ≤ 3 J(R, a, (μσ₀)^{-1/2}e, (μσ₀)^{1/2}e)
    + K₁ (μσ₀)^{-1} λ_{3/8,2}^{-1}(R;a) (V R + 3^{-2H} ‖∇h‖²)
    + K₁ 3^{-2H} λ_{3/8,2}^{-2}(R;a) ‖∇h‖² ,

together with a nonnegative value budget V whose depth-H descendant average is at most ‖h‖²_{L²(□₀)}.

This is precisely the conditional J-sensitivity of the frozen theorem responseJ_sensitivity at δ = 1, transplanted from the root cube to a mesoscopic cube:

• the factor 3 = 1 + δ + (gate) needs the mesoscopic smallness gate, which the mesoscopic depth supplies unconditionally — exactly as Provider.LambdaUnconditional.deep_cube_smallness does for the λ half;
• the Term A error carries |p|² = (μσ₀)^{-1} and must be priced against the cube-local L² value budget V R plus the scale-damped gradient 3^{-2H} ‖∇h‖², not against the root W^{1,∞} value norm: the aggregation below is false with the undamped root W^{1,∞} norm in that slot;
• the Term BC error carries |p·q| = 1 and the two damped gauges.

Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers. There is no public provider for the frozen theorem here: hcube is not discharged.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.responseJ_sensitivity_unconditional_of_mesoscale_cube_sensitivity {d : ℕ} (dimension : 2 ≤ d) (hcube : ∃ (C₀ : ℝ) (K₁ : ℝ), 1 ≤ C₀ ∧ 0 ≤ K₁ ∧ ∀ (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d), (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a → (G.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1) → ∀ (s μ σ0 : ℝ) (e : HCPolySupport.Vec d), 0 < s → s ≤ 1 / 4 → 0 < μ → 0 < σ0 → HCPolySupport.Book.Ch02.vecNorm e = 1 → ∃ (V : HCPolySupport.TriadicCube d → ℝ), (∀ (R : HCPolySupport.TriadicCube d), 0 ≤ V R) ∧ HCPolySupport.descendantsAverage (HCPolySupport.originCube d 0) (Mesoscale.mesoscaleDepth s (1 + C₀ * (h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹))) V ≤ h.valueL2 ^ 2 ∧ ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d 0) (Mesoscale.mesoscaleDepth s (1 + C₀ * (h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹))), HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (G.coeffOn R) ((√(μ * σ0))⁻¹ • e) (√(μ * σ0) • e) ≤ 3 * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) ((√(μ * σ0))⁻¹ • e) (√(μ * σ0) • e) + K₁ * ((μ * σ0)⁻¹ * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ * (V R + Real.rpow 3 (-(2 * ↑(Mesoscale.mesoscaleDepth s (1 + C₀ * (h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹))))) * h.gradientW1Infinity ^ 2)) + K₁ * (Real.rpow 3 (-(2 * ↑(Mesoscale.mesoscaleDepth s (1 + C₀ * (h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹))))) * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ ^ 2 * h.gradientW1Infinity ^ 2)) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.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)) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1) ((√(μ * σ0))⁻¹ • e) (√(μ * σ0) • e) ≤ C * μ⁻¹ * (1 + h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹).rpow (2 * t / (1 - 2 * s)) * Frozen.Section24.unitCubeHomogenizationError t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a (HCPolySupport.scalarMatrix σ0) ^ 2 + C * μ⁻¹ * σ0 * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * (1 + h.gradientW1Infinity * (Frozen.Section24.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 * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹) ^ 2

The unconditional response estimate, modulo the per-mesoscopic-cube conditional J-sensitivity.

The conclusion is the frozen statement of Algsuperdiff.Frozen.Section24.responseJ_sensitivity_unconditional verbatim. The single hypothesis hcube is the missing analytic input; see the module docstring.