Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.OriginCubeEllipticRecovery.QuadraticMu

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

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

Origin-cube elliptic recovery -- quadraticity of Mu on the centered cube #

Private sigmaStarCoarse / volumeAverage helpers, quadraticity of Mu on the centered open cube packaged from recovery data, existence of coarse block matrices, and the HasOriginCubeResponseJ{Block,PureFlux,PureGradient}QuadraticDataAtScale structures and their construction from hasQuadraticMu.

source
theorem HCPolySupport.isSigmaStarCoarse_sigmaStarCoarse_of_isSigmaStarInvCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hSInv : IsSigmaStarInvCoarse U a (sigmaStarInvCoarse U a)) (hdetInv : IsUnit (Matrix.det (sigmaStarInvCoarse U a))) :
IsSigmaStarCoarse U a (sigmaStarCoarse U a)
source
theorem HCPolySupport.isKappaCoarse_kappaCoarse_of_isSigmaStarInvKappaCoarse_of_isUnit_det_sigmaStarInvCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hM : IsSigmaStarInvKappaCoarse U a (sigmaStarInvKappaCoarse U a)) (hdetInv : IsUnit (Matrix.det (sigmaStarInvCoarse U a))) :
IsKappaCoarse U a (sigmaStarCoarse U a) (kappaCoarse U a)
source
theorem HCPolySupport.isSigmaStarInvKappaCoarse_neg_coarseBlockMatrix_lowerLeft_of_exact_slices {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) (hMuRespQ : ∀ (q : Vec d), Mu U (0, q) a = ResponseJ U 0 q a) (hMuRespP : ∀ (p : Vec d), Mu U (p, 0) a = ResponseJ U p 0 a) (hResp : ∀ (p q : Vec d), ResponseJ U p q a = Mu U (-p, q) a - vecDot p q) :
IsSigmaStarInvKappaCoarse U a (-(coarseBlockMatrix U a).lowerLeft)
source
theorem HCPolySupport.volumeAverage_le_volumeAverage_of_le_on {d : ℕ} {U : Set (Vec d)} {f g : Vec d → ℝ} (hU : MeasurableSet U) (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g U MeasureTheory.volume) (hfg : ∀ x ∈ U, f x ≤ g x) :
volumeAverage U f ≤ volumeAverage U g
source
theorem HCPolySupport.vecNormSq_volumeAverage_le_volumeAverage_vecNormSq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) {f : Vec d → Vec d} (hf : MemVectorL2 U f) :
(vecNormSq fun (i : Fin d) => volumeAverage U fun (x : Vec d) => f x i) ≤ volumeAverage U fun (x : Vec d) => vecNormSq (f x)
source
theorem HCPolySupport.hasQuadraticMu_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) :
HasQuadraticMu (openCubeSet (originCube d n)) a

Deterministic quadratic well-posedness of Mu on the centered open cube, obtained from the packaged recovery-plus-ellipticity data.

source
theorem HCPolySupport.exists_coarseBlockMatrix_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) :
∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet (originCube d n)) a Abar

Deterministic existence of the coarse block matrix on the centered open cube, obtained from the packaged recovery-plus-ellipticity data.

source
structure HCPolySupport.HasOriginCubeResponseJBlockQuadraticDataAtScale {d : ℕ} (n m : ℤ) (lam Lam : ℝ) (a : CoeffField d) :
Prop

Minimal deterministic input for the response-side block-quadratic lane on the origin cube at scale m and all of its scale-n descendants.

This is the weakest bundled package currently needed to feed the deterministic responseJ_blockQuadratic subadditivity machinery behind the annealed block/starred monotonicity theorem family.

Instances For
    source
    theorem HCPolySupport.hasOriginCubeResponseJBlockQuadraticData_of_hasQuadraticMu {d : ℕ} {n m : ℤ} {lam Lam : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d m)) a) (hQuadQ : HasQuadraticMu (openCubeSet (originCube d m)) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet (originCube d m)) p q a = Mu (openCubeSet (originCube d m)) (-p, q) a - vecDot p q) (hQuadDesc : ∀ R ∈ descendantsAtScale (originCube d m) n, HasQuadraticMu (openCubeSet R) a) (hRespDesc : ∀ R ∈ descendantsAtScale (originCube d m) n, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = Mu (openCubeSet R) (-p, q) a - vecDot p q) :
    HasOriginCubeResponseJBlockQuadraticDataAtScale n m lam Lam a

    If Mu is quadratic on the coarse open cube and its scale-n descendants, then the full mixed response identity ResponseJ(U;p,q,a) = Mu(U;(-p,q),a) - p·q upgrades directly to the public response-side block-quadratic package.

    source
    structure HCPolySupport.HasOriginCubeResponseJPureFluxQuadraticDataAtScale {d : ℕ} (n m : ℤ) (lam Lam : ℝ) (a : CoeffField d) :
    Prop

    Minimal deterministic input for the scalar \sigma_*^{-1} monotonicity lane on the origin cube at scale m and all of its scale-n descendants.

    Unlike HasOriginCubeResponseJBlockQuadraticDataAtScale, this package only asks for the pure-flux slice ResponseJ(U; 0, q) to match the lower-right quadratic form of the coarse block matrix.

    Instances For
      source
      structure HCPolySupport.HasOriginCubeResponseJPureGradientQuadraticDataAtScale {d : ℕ} (n m : ℤ) (lam Lam : ℝ) (a : CoeffField d) :
      Prop

      Minimal deterministic input for the scalar B monotonicity lane on the origin cube at scale m and all of its scale-n descendants.

      This keeps only the pure-gradient slice ResponseJ(U; p, 0), which is enough for the upper-left scalar observable but does not carry the full block quadratic response package.

      Instances For
        source
        theorem HCPolySupport.hasOriginCubeResponseJPureFluxQuadraticData_of_hasQuadraticMu {d : ℕ} {n m : ℤ} {lam Lam : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d m)) a) (hQuadQ : HasQuadraticMu (openCubeSet (originCube d m)) a) (hMuRespQ : ∀ (q : Vec d), Mu (openCubeSet (originCube d m)) (0, q) a = ResponseJ (openCubeSet (originCube d m)) 0 q a) (hQuadDesc : ∀ R ∈ descendantsAtScale (originCube d m) n, HasQuadraticMu (openCubeSet R) a) (hMuRespDesc : ∀ R ∈ descendantsAtScale (originCube d m) n, ∀ (q : Vec d), Mu (openCubeSet R) (0, q) a = ResponseJ (openCubeSet R) 0 q a) :
        HasOriginCubeResponseJPureFluxQuadraticDataAtScale n m lam Lam a

        If Mu is already known to be quadratic on the coarse open cube and its scale-n descendants, then the exact pure-flux identities Mu(U; (0, q), a) = ResponseJ(U; 0, q, a) upgrade directly to the public response-side \sigma_*^{-1} slice package.

        source
        theorem HCPolySupport.hasOriginCubeResponseJPureGradientQuadraticData_of_hasQuadraticMu {d : ℕ} {n m : ℤ} {lam Lam : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d m)) a) (hQuadQ : HasQuadraticMu (openCubeSet (originCube d m)) a) (hMuRespQ : ∀ (p : Vec d), Mu (openCubeSet (originCube d m)) (p, 0) a = ResponseJ (openCubeSet (originCube d m)) p 0 a) (hQuadDesc : ∀ R ∈ descendantsAtScale (originCube d m) n, HasQuadraticMu (openCubeSet R) a) (hMuRespDesc : ∀ R ∈ descendantsAtScale (originCube d m) n, ∀ (p : Vec d), Mu (openCubeSet R) (p, 0) a = ResponseJ (openCubeSet R) p 0 a) :
        HasOriginCubeResponseJPureGradientQuadraticDataAtScale n m lam Lam a

        If Mu is already known to be quadratic on the coarse open cube and its scale-n descendants, then the exact pure-gradient identities Mu(U; (p, 0), a) = ResponseJ(U; p, 0, a) upgrade directly to the public response-side B slice package.