Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch02.Theorems.Dilation

Coarse-graining support: Support.Book.Ch02.Theorems.Dilation #

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

source
theorem HCPolySupport.Book.Ch02.dilateCube_neg_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) :
dilateCube (-k) (dilateCube k Q) = Q

A cube dilated by 3^k and then by 3^{-k} returns to itself.

source
theorem HCPolySupport.Book.Ch02.dilateCube_dilateCube_neg {d : ℕ} (k : ℤ) (Q : TriadicCube d) :
dilateCube k (dilateCube (-k) Q) = Q

A cube dilated by 3^{-k} and then by 3^k returns to itself.

source
theorem HCPolySupport.Book.Ch02.dilateCube_neg_scale_scale {d : ℕ} (Q : TriadicCube d) :
(dilateCube (-Q.scale) Q).scale = 0

Normalizing a cube by dilation through -Q.scale gives a scale-zero cube.

source
theorem HCPolySupport.Book.Ch02.dilateVec_mem_openCubeSet_dilateCube {d : ℕ} (k : ℤ) {Q : TriadicCube d} {x : Vec d} (hx : x ∈ openCubeSet Q) :
dilateVec k x ∈ openCubeSet (dilateCube k Q)

Dilation by 3 ^ k maps points of a triadic cube into points of the dilated triadic cube.

source
theorem HCPolySupport.Book.Ch02.dilateVec_neg_dilateVec {d : ℕ} (k : ℤ) (x : Vec d) :
dilateVec (-k) (dilateVec k x) = x

Dilation by 3^{-k} is the inverse of dilation by 3^k.

source
theorem HCPolySupport.Book.Ch02.dilateVec_dilateVec_neg {d : ℕ} (k : ℤ) (x : Vec d) :
dilateVec k (dilateVec (-k) x) = x

Dilation by 3^k is the inverse of dilation by 3^{-k}.

source
theorem HCPolySupport.Book.Ch02.openCubeSet_undilate_subset_of_subset {d : ℕ} (k : ℤ) {Q R : TriadicCube d} (hsub : openCubeSet R ⊆ openCubeSet Q) :
openCubeSet (dilateCube (-k) R) ⊆ openCubeSet (dilateCube (-k) Q)

Undilating preserves cube containment relations.

source
theorem HCPolySupport.Book.Ch02.eventuallyEq_comp_undilate_of_ae_eq {d : ℕ} (k : ℤ) {Q : TriadicCube d} {f g : Vec d → Mat d} (hfg : f =ᵐ[volumeMeasureOn (openCubeSet Q)] g) :
(fun (x : Vec d) => f (undilateVec k x)) =ᵐ[volumeMeasureOn (openCubeSet (dilateCube k Q))] fun (x : Vec d) => g (undilateVec k x)

Pull an a.e. coefficient-field equality forward to the dilated cube.

source
noncomputable def HCPolySupport.Book.Ch02.CoeffOn.dilate {d : ℕ} (k : ℤ) {Q : TriadicCube d} (a : CoeffOn (cubeDomain Q)) :
CoeffOn (cubeDomain (dilateCube k Q))

A concrete public coefficient object on a dilated cube.

The representative is chosen via the pointwise-good representative of the source coefficient object, but the public relation below records only the intended a.e. pullback relation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Book.Ch02.CoeffOn.dilate_isCubeDilation {d : ℕ} (k : ℤ) {Q : TriadicCube d} (a : CoeffOn (cubeDomain Q)) :
    IsCubeDilation k a (dilate k a)

    The concrete dilated coefficient object is a public a.e. cube dilation.

    source
    theorem HCPolySupport.Book.Ch02.CoeffOn.dilate_restrictsTo {d : ℕ} (k : ℤ) {Q R : TriadicCube d} {aQ : CoeffOn (cubeDomain Q)} {aR : CoeffOn (cubeDomain R)} (hsub : openCubeSet R ⊆ openCubeSet Q) (h : aQ.RestrictsTo aR) :
    (dilate k aQ).RestrictsTo (dilate k aR)

    Dilation preserves public a.e. restriction of coefficient objects.

    source
    noncomputable def HCPolySupport.Book.Ch02.TriadicCoeffFamily.dilatedCoeffOnAt {d : ℕ} (k : ℤ) (a : TriadicCoeffFamily d) (R : TriadicCube d) :
    CoeffOn (cubeDomain R)

    The coefficient object assigned to a target cube by the dilated coefficient family. The source cube is the undilated target cube.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def HCPolySupport.Book.Ch02.TriadicCoeffFamily.dilate {d : ℕ} (k : ℤ) (a : TriadicCoeffFamily d) :
      TriadicCoeffFamily d

      The public coefficient-family dilation by 3^k.

      Equations
      Instances For
        source
        theorem HCPolySupport.Book.Ch02.TriadicCoeffFamily.isDilation_dilate {d : ℕ} (k : ℤ) (a : TriadicCoeffFamily d) :
        IsDilation k a (dilate k a)

        The concrete coefficient-family dilation satisfies the public dilation relation.

        source
        theorem HCPolySupport.Book.Ch02.coarseBlockMatrix_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) :
        coarseBlockMatrix (cubeDomain (dilateCube k Q)) b = coarseBlockMatrix (cubeDomain Q) a

        The coarse doubled block matrix is invariant under public cube dilation.

        source
        theorem HCPolySupport.Book.Ch02.doubledMu_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (P : BlockVec d) :
        doubledMu (cubeDomain (dilateCube k Q)) b P = doubledMu (cubeDomain Q) a P

        The doubled Dirichlet energy mu is invariant under public cube dilation.

        source
        theorem HCPolySupport.Book.Ch02.doubledResponseJ_dilate {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {b : CoeffOn (cubeDomain (dilateCube k Q))} (hCoeff : CoeffOn.IsCubeDilation k a b) (P R : BlockVec d) :
        doubledResponseJ (cubeDomain (dilateCube k Q)) b P R = doubledResponseJ (cubeDomain Q) a P R

        The doubled response Jbold is invariant under public cube dilation.

        source
        theorem HCPolySupport.Book.Ch02.dilateCube_injective {d : ℕ} (k : ℤ) :
        Function.Injective (dilateCube k)

        Dilation of triadic cubes is injective.

        source
        theorem HCPolySupport.Book.Ch02.childCubes_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) :
        childCubes (dilateCube k Q) = Finset.image (dilateCube k) (childCubes Q)

        Children commute with dilation by 3^k.

        source
        theorem HCPolySupport.Book.Ch02.descendantsAtDepth_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) (n : ℕ) :
        descendantsAtDepth (dilateCube k Q) n = Finset.image (dilateCube k) (descendantsAtDepth Q n)

        Descendants at fixed depth commute with dilation by 3^k.

        source
        theorem HCPolySupport.Book.Ch02.descendantsAtScale_dilateCube {d : ℕ} (k n : ℤ) (Q : TriadicCube d) :
        descendantsAtScale (dilateCube k Q) (n + k) = Finset.image (dilateCube k) (descendantsAtScale Q n)

        Descendants at scale n commute with dilation, with scale shifted by k.

        source
        theorem HCPolySupport.Book.Ch02.coarseBMatrixNorm_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) :
        coarseBMatrixNorm (dilateCube k Q) b = coarseBMatrixNorm Q a

        One-cube upper coarse-matrix norm is dilation invariant.

        source
        theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) :
        coarseSigmaStarInvMatrixNorm (dilateCube k Q) b = coarseSigmaStarInvMatrixNorm Q a

        One-cube lower coarse-matrix norm is dilation invariant.

        source
        theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) :
        maxDescendantBMatrixNormAtScale (dilateCube k Q) (n + k) b = maxDescendantBMatrixNormAtScale Q n a

        The descendant maximum of |b| is dilation invariant, with scale shift.

        source
        theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) :
        maxDescendantSigmaStarInvMatrixNormAtScale (dilateCube k Q) (n + k) b = maxDescendantSigmaStarInvMatrixNormAtScale Q n a

        The descendant maximum of |sigma_*^{-1}| is dilation invariant.

        source
        theorem HCPolySupport.Book.Ch02.LambdaSqFinite_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s q : ℝ) :
        LambdaSqFinite (dilateCube k Q) s q b = LambdaSqFinite Q s q a
        source
        theorem HCPolySupport.Book.Ch02.lambdaSqFinite_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s q : ℝ) :
        lambdaSqFinite (dilateCube k Q) s q b = lambdaSqFinite Q s q a
        source
        theorem HCPolySupport.Book.Ch02.LambdaSqInfinity_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s : ℝ) :
        LambdaSqInfinity (dilateCube k Q) s b = LambdaSqInfinity Q s a
        source
        theorem HCPolySupport.Book.Ch02.lambdaSqInfinity_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s : ℝ) :
        lambdaSqInfinity (dilateCube k Q) s b = lambdaSqInfinity Q s a
        source
        theorem HCPolySupport.Book.Ch02.LambdaSq_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) :
        LambdaSq (dilateCube k Q) s q b = LambdaSq Q s q a

        Coarse upper ellipticity is dilation invariant.

        source
        theorem HCPolySupport.Book.Ch02.lambdaSq_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) :
        lambdaSq (dilateCube k Q) s q b = lambdaSq Q s q a

        Coarse lower ellipticity is dilation invariant.

        source
        theorem HCPolySupport.Book.Ch02.LambdaS_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s : ℝ) :
        LambdaS (dilateCube k Q) s b = LambdaS Q s a
        source
        theorem HCPolySupport.Book.Ch02.lambdaS_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s : ℝ) :
        lambdaS (dilateCube k Q) s b = lambdaS Q s a
        source
        theorem HCPolySupport.Book.Ch02.ThetaRatio_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s t : ℝ) :
        ThetaRatio (dilateCube k Q) s t b = ThetaRatio Q s t a
        source
        theorem HCPolySupport.Book.Ch02.maxDescendantUpperEllipticityAtScale_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (q : MultiscaleExponent) :
        maxDescendantUpperEllipticityAtScale (dilateCube k Q) (n + k) s q b = maxDescendantUpperEllipticityAtScale Q n s q a
        source
        theorem HCPolySupport.Book.Ch02.maxDescendantLowerEllipticityInvAtScale_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (q : MultiscaleExponent) :
        maxDescendantLowerEllipticityInvAtScale (dilateCube k Q) (n + k) s q b = maxDescendantLowerEllipticityInvAtScale Q n s q a
        source
        theorem HCPolySupport.Book.Ch02.normalizedBlockResponseValueSet_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (a0 : Mat d) :
        normalizedBlockResponseValueSet (dilateCube k Q) b a0 = normalizedBlockResponseValueSet Q a a0
        source
        theorem HCPolySupport.Book.Ch02.normalizedBlockResponseMax_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (a0 : Mat d) :
        normalizedBlockResponseMax (dilateCube k Q) b a0 = normalizedBlockResponseMax Q a a0
        source
        theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) (a0 : Mat d) :
        maxDescendantNormalizedBlockResponseAtScale (dilateCube k Q) (n + k) b a0 = maxDescendantNormalizedBlockResponseAtScale Q n a a0
        source
        theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) (p : MultiscaleExponent) (a0 : Mat d) :
        scaleResponseAtScale (dilateCube k Q) (n + k) p b a0 = scaleResponseAtScale Q n p a a0
        source
        theorem HCPolySupport.Book.Ch02.HomogenizationErrorFinite_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (q : ℝ) (a0 : Mat d) :
        HomogenizationErrorFinite (dilateCube k Q) (n + k) s p q b a0 = HomogenizationErrorFinite Q n s p q a a0
        source
        theorem HCPolySupport.Book.Ch02.HomogenizationErrorInfinity_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (a0 : Mat d) :
        HomogenizationErrorInfinity (dilateCube k Q) (n + k) s p b a0 = HomogenizationErrorInfinity Q n s p a a0
        source
        theorem HCPolySupport.Book.Ch02.HomogenizationError_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d) :
        HomogenizationError (dilateCube k Q) (n + k) s p q b a0 = HomogenizationError Q n s p q a a0
        source
        theorem HCPolySupport.Book.Ch02.HomogenizationErrorOnCube_dilate {d : ℕ} {k : ℤ} {a b : TriadicCoeffFamily d} (h : TriadicCoeffFamily.IsDilation k a b) (Q : TriadicCube d) (s : ℝ) (p q : MultiscaleExponent) (a0 : Mat d) :
        HomogenizationErrorOnCube (dilateCube k Q) s p q b a0 = HomogenizationErrorOnCube Q s p q a a0
        source
        theorem HCPolySupport.Book.Ch02.cubeDilationTheory (d : ℕ) :
        CubeDilationTheory d

        Proved one-cube dilation theorem package.

        source
        theorem HCPolySupport.Book.Ch02.multiscaleDilationTheory (d : ℕ) [NeZero d] :
        MultiscaleDilationTheory d

        Proved Chapter 2.5 multiscale dilation theorem package.

        source
        theorem HCPolySupport.Book.Ch02.dilationTheory (d : ℕ) [NeZero d] :
        DilationTheory d

        Aggregate proved public dilation theorem package.