Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.OriginCubeEllipticRecovery.Setup

Coarse-graining support: Support.CoarseGraining.OriginCubeEllipticRecovery.Setup #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Origin-cube elliptic recovery -- volume lemmas, data package, descendant family #

Basic volume-of-centered-cube lemmas, the HasOpenCubeEllipticRecoveryData package, the canonical instance from an elliptic field, and the descendant recovery family used downstream.

source
theorem HCPolySupport.volume_openCubeSet_originCube_lt_top {d : ℕ} (n : ℤ) :
MeasureTheory.volume (openCubeSet (originCube d n)) < ⊤

The centered open cube has finite Lebesgue measure.

This is the finite-volume input needed to instantiate the L² and recovery machinery on openCubeSet (originCube d n).

source
theorem HCPolySupport.volume_openCubeSet_originCube_toReal_pos {d : ℕ} (n : ℤ) :
0 < (MeasureTheory.volume (openCubeSet (originCube d n))).toReal

The centered open cube has strictly positive Lebesgue volume.

This is the normalization hypothesis required by the deterministic doubled operator construction from ellipticity.

source
def HCPolySupport.originCubeScaleTranslationShift {d : ℕ} (k : ℤ) (Q : TriadicCube d) :
Fin d → ℤ

Integer translation shift identifying a nonnegative-scale triadic cube with the corresponding translated origin cube.

Equations
Instances For
    source
    def HCPolySupport.HasOpenCubeEllipticRecoveryData {d : ℕ} (n : ℤ) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} (a : CoeffField d) :
    Prop

    Package the deterministic hypotheses that upgrade raw ellipticity on the centered open cube to the compatibility data needed by the Mu recovery machinery.

    The recovery space R is fixed once and for all on the domain openCubeSet (originCube d n). For a given coefficient field a, this predicate asks for:

    1. an ellipticity witness for a on that domain;
    2. the compatibility data identifying the note's Mu with the Hilbert-space minimization problem built from that ellipticity witness.
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.hasOpenCubeEllipticRecoveryData_of_isEllipticFieldOn_of_mu_eq_muCandidate {d : ℕ} (n : ℤ) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (mu_eq_muCandidate : ∀ (P : BlockVec d), Mu (openCubeSet (originCube d n)) P a = (R.toMuHilbertRealization (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)).muCandidate P) :
      HasOpenCubeEllipticRecoveryData n R a

      Build the origin-cube recovery package from ellipticity and the single remaining hard compatibility field Mu = muCandidate.

      The pairing-integrability part of HasOpenCubeEllipticRecoveryData is already automatic from ellipticity and the L² control of recovered fields.

      source
      def HCPolySupport.OpenCubeDescendantEllipticRecoveryFamily {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} :
      Prop

      Descendant-family version of HasOpenCubeEllipticRecoveryData.

      This packages the translated origin-cube recovery input on every descendant of the parent cube Q. It is the natural upstream hypothesis for producing the deterministic Chapter-2 coarse data needed by the top Chapter-3 coarse Poincare wrappers.

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