GaugeBridge

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

Coarse Poincaré at the sensitivity gauge (s, q) = (3/8, 2)

Two layers are proved:

• the general layer, at an arbitrary triadic cube Q and an arbitrary CoarseGraining coefficient family F, in CoarseGraining gauge vocabulary (Ch02.lambdaSq Q s q F);
• the frozen unit-cube layer, obtained from the general layer by choosing a compatible family (exists_compatibleTriadicCoeffFamily) and rewriting the gauge with unitCubeLambda_characterization.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.rpow_neg_half_eq_sqrt_inv {x : ℝ} (hx : 0 ≤ x) : x.rpow (-(1 / 2)) = √x⁻¹

x ^ (-(1/2)) is √(x⁻¹) for nonnegative x, including at x = 0.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.sensitivityExponent_isAdmissible : (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2).IsAdmissible

The gauge exponent pair used by the frozen sensitivity statements.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.poincareDiscountFactor_sensitivity_pos : 0 < HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2)

The scale-free discount factor of the coarse Poincaré right-hand side at the sensitivity gauge is positive.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.scaleNormalizedNegativeBesovVectorNorm_solutionGradient_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch03.CoeffFamily d) {p q : HCPolySupport.Vec d} {v : HCPolySupport.Book.Ch03.CubeSolution Q F} (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p q v) : HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm Q (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch03.solutionGradientField v) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * √(HCPolySupport.Book.Ch02.lambdaSq Q (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ * (2 * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p q))

General coarse Poincaré at the sensitivity gauge. At an arbitrary triadic cube and an arbitrary coefficient family, the concrete negative Besov norm of the gradient of a response maximizer is controlled by λ_{3/8,2}^{-1/2} √J, up to the scale-free discount constant.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.scaleNormalizedNegativeBesovVectorNorm_solutionGradient_unitCube_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {p q : HCPolySupport.Vec d} (F : HCPolySupport.Book.Ch03.CoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {v : HCPolySupport.Book.Ch03.CubeSolution (HCPolySupport.originCube d 0) F} (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (F.coeffOn (HCPolySupport.originCube d 0)) p q v) : HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm (HCPolySupport.originCube d 0) (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch03.solutionGradientField v) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * √(Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * (2 * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q))

Frozen unit-cube coarse Poincaré at the sensitivity gauge. The same estimate with the frozen gauge unitCubeLambda (3/8) (.finite 2) a, for a coefficient given directly on the origin cube.