Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.PrintOrderNearIdentityDualAbsorption

High-contrast homogenization: Provider.Regularity.PrintOrderNearIdentityDualAbsorption #

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

Near-identity absorption for cube full-dual regularity #

An A-solenoidal potential field is an identity-solenoidal field after the defect (A - I)w is moved into the datum. The estimates below isolate the exact smallness coefficient required by this reduction.

source
def HCPolySupport.HighContrast.PrintOrderIdentityCubeDualRegularityWithConstant (d : ℕ) (g Cid : ℝ) :
Prop

Identity-coefficient cube dual regularity with a named uniform constant, at the order selected after g.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.identityActionSmallness_of_opNorm_defect {d : ℕ} {Cid eps : ℝ} (hCid : 0 ≤ Cid) (hsmall : Cid * (↑d ^ 2 * eps) ≤ 1 / 2) {E : Mat d} (hE : ‖E‖ ≤ eps) :
    Cid * dualBesovMatrixActionSize E ≤ 1 / 2

    The operator-norm defect bound implies the action-size smallness needed by the component-sum full-dual norm.

    source
    theorem HCPolySupport.HighContrast.printOrder_dual_bounds_of_identity_of_action_absorption {d : ℕ} {g Cid B : ℝ} (hg : g ∈ Set.Ico 0 1) (hidentity : PrintOrderIdentityCubeDualRegularityWithConstant d g Cid) {A : Mat d} (hAaction : dualBesovMatrixActionSize A ≤ B) (hB : 0 ≤ B) (hsmall : Cid * dualBesovMatrixActionSize (A - 1) ≤ 1 / 2) (Q : TriadicCube d) {w F : Vec d → Vec d} (hF : MemVectorL2 (cubeSet Q) F) (hw : IsPotentialZeroTraceOn (cubeSet Q) w) (hsol : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul A (w x) + F x) :
    (cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q (printCertificateOrder g) fun (x : Vec d) => matVecMul A (w x)) ≤ B * (2 * Cid) * cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q (printCertificateOrder g) F ∧ (cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q (printCertificateOrder g) fun (x : Vec d) => matVecMul A (w x) + F x) ≤ 2 * Cid * cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q (printCertificateOrder g) F

    Quantitative perturbation lemma for one constant matrix and one cube. The first coefficient also carries an upper bound for the action of A; the second coefficient is the absorbed identity constant.