Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.PrintOrderParametricRoundedAbsorptionRepair

High-contrast homogenization: Provider.Regularity.PrintOrderParametricRoundedAbsorptionRepair #

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

Parametric rounded-reference repair for perturbative absorption #

The rounded grid is defined at every generation above kZero d. This file states the exact constructor strengthening needed to select that generation after the identity-regularity constant is known. No claim is made that the canonical generation already satisfies the strengthened tolerance.

source
noncomputable def HCPolySupport.HighContrast.roundedReferenceMatrixAtGeneration {d : ℕ} (l : ℤ) (abar : Mat d) (_hS : Matrix.PosDef (symmPart abar)) :
Mat d

The constant rounded reference obtained from an arbitrary admissible rounding generation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HCPolySupport.HighContrast.printOrderAbsorptionEffectiveIdentityConstant (d : ℕ) (Cid : ℝ) :
    ℝ

    The identity constant enlarged by the component-sum matrix-action cost. The lower bound by one makes the tightened tolerance positive even when the identity estimate has zero constant.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.printOrderAbsorptionTolerance (d : ℕ) (Cid : ℝ) :
      ℝ

      The constructor tolerance selected after the effective identity constant is known.

      Equations
      Instances For
        source
        theorem HCPolySupport.HighContrast.printOrderAbsorptionEffectiveIdentityConstant_pos (d : ℕ) (Cid : ℝ) :
        0 < printOrderAbsorptionEffectiveIdentityConstant d Cid
        source
        theorem HCPolySupport.HighContrast.printOrderAbsorptionTolerance_pos (d : ℕ) (Cid : ℝ) :
        0 < printOrderAbsorptionTolerance d Cid
        source
        theorem HCPolySupport.HighContrast.printOrderAbsorptionTolerance_le_half (d : ℕ) (Cid : ℝ) :
        printOrderAbsorptionTolerance d Cid ≤ 1 / 2
        source
        theorem HCPolySupport.HighContrast.printOrderAbsorptionTolerance_smallness (d : ℕ) (Cid : ℝ) :
        Cid * (↑d ^ 2 * printOrderAbsorptionTolerance d Cid) ≤ 1 / 2

        The tightened tolerance gives precisely the absorption coefficient needed by the component-sum full-dual norm.

        source
        def HCPolySupport.HighContrast.PrintOrderRoundedReferenceConstructorAtTolerance (d : ℕ) (eps : ℝ) :
        Prop

        Exact constructor-side repair: select a rounded generation after the desired defect tolerance is known, retaining a uniform ellipticity window. The first conjunct records the symmetric positive reference required by the constant-coefficient carrier.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def HCPolySupport.HighContrast.PrintOrderRoundedReferenceDualRegularityAtGeneration (d : ℕ) (g : ℝ) (l : ℤ) :
          Prop

          Consumer surface for a rounded reference whose generation is selected after the identity constant.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For