Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.FiniteCubeSolutionRestriction

High-contrast homogenization: Provider.Regularity.FiniteCubeSolutionRestriction #

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

Restriction of centered-cube solutions #

This module restricts a coefficient-harmonic solution on one centered triadic cube to any smaller centered triadic cube and transports the coefficient representative supplied by the compatible coefficient family.

source
theorem HCPolySupport.HighContrast.centralDescendant_originCube_eq_originCube_sub {d : ℕ} (m : ℤ) (j : ℕ) :
CubeCalderonZygmund.centralDescendant (originCube d m) j = originCube d (m - ↑j)

A central descendant of a centered cube is the centered cube at the corresponding lower scale.

source
theorem HCPolySupport.HighContrast.originCube_mem_descendantsAtDepth_of_le {d : ℕ} {n m : ℤ} (hnm : n ≤ m) :
originCube d n ∈ descendantsAtDepth (originCube d m) (m - n).toNat

The smaller centered cube is a descendant of the larger centered cube at the integer scale gap.

source
theorem HCPolySupport.HighContrast.openCubeSet_originCube_subset_of_le {d : ℕ} {n m : ℤ} (hnm : n ≤ m) :
openCubeSet (originCube d n) ⊆ openCubeSet (originCube d m)

Centered open cubes are nested in their scale parameter.

source
noncomputable def HCPolySupport.HighContrast.finiteCubeSolutionRestriction {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) :
Book.Ch03.CubeSolution (originCube d n) a

Restrict a solution on Q_m to the centered subcube Q_n, retaining the compatible coefficient representative on Q_n.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.finiteCubeSolutionRestriction_toFun {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) :
    (finiteCubeSolutionRestriction a hnm u).toH1.toFun = u.toH1.toFun

    Restriction preserves the original value representative.

    source
    @[simp]
    theorem HCPolySupport.HighContrast.finiteCubeSolutionRestriction_grad {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) :
    (finiteCubeSolutionRestriction a hnm u).toH1.grad = u.toH1.grad

    Restriction preserves the original gradient representative.