Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants

Shared sensitivity constants #

Common pairing and zero-trace constants extracted from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46 for the flux and difference-quotient routes.

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.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.

source
noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.zeroTraceValueConst (d : ℕ) :
ℝ

The constant of the zero-trace L² estimate at the gauge exponent.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.zeroTraceValueConst_nonneg (d : ℕ) :
    0 ≤ zeroTraceValueConst d
    source
    noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.besovPairingConstant (d : ℕ) :
    ℝ

    The Besov pairing constant at the shared sensitivity gauge.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.besovPairingConstant_pos (d : ℕ) :
      0 < besovPairingConstant d
      source
      theorem Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.sqrt_vecNormSq_le_sqrt_dimension_mul_norm {d : ℕ} (x : HCPolySupport.Vec d) :
      √(HCPolySupport.vecNormSq x) ≤ √↑d * ‖x‖

      Euclidean vector length is bounded by sqrt dimension times the coordinate sup norm.