Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.ConvexHardyScaleSummation

High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyScaleSummation #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Dyadic scale summation for convex-domain Hardy chains #

The radius cutoff on a chain link turns a growing dyadic scale factor into a finite geometric head. The remaining distance from the initial link carries a decaying geometric tail. Their product is bounded uniformly in the physical radius and in the reference interior-ball radius.

source
noncomputable def HCPolySupport.HighContrast.convexHardyDyadicRadius (rho : ℝ) (n : ℕ) :
ℝ

The dyadic radius at depth n below a reference radius.

Equations
Instances For
    source
    def HCPolySupport.HighContrast.convexHardyScaleExponent (d : ℕ) (s : ℝ) :
    ℝ

    The scale exponent left after combining the two Hardy radii.

    Equations
    Instances For
      source
      def HCPolySupport.HighContrast.convexHardyScaleGap (s beta : ℝ) :
      ℝ

      The positive exponent gap between fractional decay and chain weights.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.convexHardyScaleInnerRatio (s beta : ℝ) :
        ℝ

        The decaying ratio along links below a fixed dyadic scale.

        Equations
        Instances For
          source
          noncomputable def HCPolySupport.HighContrast.convexHardyScaleOuterRatio (d : ℕ) (s : ℝ) :
          ℝ

          The growing ratio of consecutive dyadic scale heads.

          Equations
          Instances For
            source
            noncomputable def HCPolySupport.HighContrast.convexHardyScaleSummationConstant (d : ℕ) (s beta D : ℝ) :
            ENNReal

            The explicit constant produced by the inner tail and the cutoff outer head.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem HCPolySupport.HighContrast.tsum_cutoff_geometric_head_le {q X C : ℝ} (hq : 1 < q) (hX : 0 ≤ X) (hC : 0 ≤ C) :
              (∑' (k : ℕ), if X * q ^ (k + 1) ≤ C then ENNReal.ofReal (X * q ^ (k + 1)) else 0) ≤ ENNReal.ofReal (q / (q - 1) * C)

              A geometric head cut off by a pointwise ceiling has uniformly bounded extended nonnegative mass.