High-contrast homogenization: Provider.Regularity.FiniteCubeEnergyRestriction

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

Normalized energy under centered-cube restriction

This module identifies the weighted gradient norm with the Chapter 3 energy norm and records the normalized-volume loss under restriction to a centered child cube.

theorem HCPolySupport.HighContrast.weightedGradNorm_eq_localSymmetricEnergyENorm {d : ℕ} (Q : TriadicCube d) (a : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain Q)) (u : H1Function (openCubeSet Q)) : weightedGradNorm a.toCoeffField (openCubeSet Q) u.grad = Book.Ch03.ABK26.localSymmetricEnergyENorm Q a u

The weighted gradient norm is the normalized local symmetric energy on a triadic cube.

theorem HCPolySupport.HighContrast.localSymmetricEnergyENorm_eq_ofReal_h1EnergyNormOnCube {d : ℕ} (Q : TriadicCube d) (a : Book.Ch03.CoeffFamily d) (u : H1Function (Book.Ch02.cubeDomain Q).carrier) : Book.Ch03.ABK26.localSymmetricEnergyENorm Q (a.coeffOn Q) u = ENNReal.ofReal (Book.Ch03.h1EnergyNormOnCube Q a u)

The local symmetric energy is the ENNReal realization of the public Chapter 3 energy norm.

theorem HCPolySupport.HighContrast.weightedGradNorm_eq_ofReal_h1EnergyNormOnCube {d : ℕ} (Q : TriadicCube d) (a : Book.Ch03.CoeffFamily d) (u : H1Function (Book.Ch02.cubeDomain Q).carrier) : weightedGradNorm (a.coeffOn Q).toCoeffField (openCubeSet Q) u.grad = ENNReal.ofReal (Book.Ch03.h1EnergyNormOnCube Q a u)

The weighted gradient norm is exactly the ENNReal realization of the public Chapter 3 cube energy norm.

theorem HCPolySupport.HighContrast.h1EnergyNormOnCube_finiteCubeSolutionRestriction_sub_one_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) : Book.Ch03.h1EnergyNormOnCube (originCube d (m - 1)) a (finiteCubeSolutionRestriction a ⋯ u).toH1 ≤ ↑(3 ^ d) * Book.Ch03.h1EnergyNormOnCube (originCube d m) a u.toH1

Restricting a centered-cube solution to its centered child loses at most the number of ordinary children in the normalized energy norm.

theorem HCPolySupport.HighContrast.h1EnergyNormOnCube_finiteCubeSolutionRestriction_sub_nat_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (N : ℕ) (u : Book.Ch03.CubeSolution (originCube d m) a) : Book.Ch03.h1EnergyNormOnCube (originCube d (m - ↑N)) a (finiteCubeSolutionRestriction a ⋯ u).toH1 ≤ ↑((3 ^ d) ^ N) * Book.Ch03.h1EnergyNormOnCube (originCube d m) a u.toH1

Restriction by an arbitrary fixed number of centered scales loses at most the corresponding power of the number of ordinary children.