Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.C1WeightedProjectionCloseness

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.C1WeightedProjectionCloseness

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

Near-identity estimate for the weighted finite-corrector projection #

Coefficient-energy minimality and the scalar good-tail average coercivity turn the quantitative finite-corrector tail into a near-identity bound for the canonical linear slope projection.

source
noncomputable def HCPolySupport.HighContrast.Root.localHarmonicEnergy {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (q : ℕ) (F : ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (localGradientCube d q)) ⋯)) :
ℝ

Normalized symmetric coefficient energy on the harmonic-gradient space of an origin cube.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Root.finiteCorrectorWeightedProjection_sub_identity_le {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (s delta c : ℝ) (n0 : ℤ) (hs : 0 < s) (hc1 : c ≤ 1) (hdelta : delta ∈ Set.Ioc 0 c) (hgood : ScalarIdentityGoodTail a s delta n0) (hcoercive : ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (q t : ℕ), n ≤ ↑q → ∀ (e : Vec d), euclideanNorm e ≤ 2 * euclideanNorm (cubeAverageVec (originCube d ↑q) (finiteAffineSolution a (↑(q + t + 2)) e).toH1.grad)) (q m : ℕ) (hnq : n0 ≤ ↑q) (hqm2 : q + 2 ≤ m) (K : ℝ) (hK : 0 ≤ K) (htail : ∀ (e : Vec d), have T := finiteTrialHarmonicGradientLinearMap a ⋯; have J := jointTargetHarmonicGradientLinearMap a hCauchy q; √(localHarmonicEnergy a q (J e - T e)) ≤ K * euclideanNorm e) :
    have hT := ⋯; have P := finiteCorrectorWeightedProjection a hCauchy ⋯ hT; ∀ (e : Vec d), euclideanNorm (P e - e) ≤ 4 * √(4 * ↑d) * K * euclideanNorm e

    The canonical coefficient-weighted projection is quantitatively close to the identity whenever the joint-to-finite tail is small.

    source
    theorem HCPolySupport.HighContrast.Root.finiteCorrectorWeightedProjection_bijective {d : ℕ} (P : Vec d →ₗ[ℝ] Vec d) (theta : ℝ) (htheta : theta < 1) (hclose : ∀ (e : Vec d), euclideanNorm (P e - e) ≤ theta * euclideanNorm e) :
    Function.Bijective ⇑P

    A strict near-identity coefficient makes the canonical weighted projection bijective and hence supplies the finite-to-infinite slope reparameterization.