Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.FiniteAffineSuccessorLocalEnergy

High-contrast homogenization: Provider.Regularity.FiniteAffineSuccessorLocalEnergy #

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

Local energy of successive finite affine solutions #

This module applies coarse Caccioppoli on a centered parent cube. Its honest core is the centered cube two scales below. The parent value oscillation is controlled by the two adjacent finite-corrector slope errors, while the local good-pair condition bounds the Caccioppoli ellipticity factors.

source
theorem HCPolySupport.HighContrast.originCube_sub_two_mem_descendantsAtDepth {d : ℕ} (m : ℤ) :
originCube d (m - 2) ∈ descendantsAtDepth (originCube d m) 2
source
noncomputable def HCPolySupport.HighContrast.finiteAffineSuccessorDifferenceInnerRestriction {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
Book.Ch03.CubeSolution (originCube d (m - 2)) a

The successive finite affine difference, restricted to the centered cube two scales below its harmonic parent.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.finiteAffineSuccessorDifferenceInnerRestriction_grad {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
    (finiteAffineSuccessorDifferenceInnerRestriction a m e).toH1.grad = (finiteAffineSuccessorDifference a m e).toH1.grad

    The inner restriction preserves the successive difference's gradient representative.

    source
    theorem HCPolySupport.HighContrast.caccioppoliCoreSet_originCube_eq_openCubeSet_sub_two {d : ℕ} (m : ℤ) :
    Book.Ch03.caccioppoliCoreSet (originCube d m) (cubeCenter (originCube d m)) = openCubeSet (originCube d (m - 2))

    On a centered cube, the coarse Caccioppoli core is exactly the centered cube two scales below.

    source
    theorem HCPolySupport.HighContrast.finiteAffineSuccessorDifferenceInner_energy_eq_coreEnergy {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) :
    Book.Ch03.h1EnergyNormOnCube (originCube d (m - 2)) a (finiteAffineSuccessorDifferenceInnerRestriction a m e).toH1 = √(Book.Ch03.interiorCaccioppoliCoreEnergy (originCube d m) a (cubeCenter (originCube d m)) (finiteAffineSuccessorDifference a m e))

    The actual inner-cube energy norm of the restricted difference is the square root of the parent Caccioppoli core energy.

    source
    theorem HCPolySupport.HighContrast.exists_finiteAffineSuccessorDifferenceLocalEnergyEstimateConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) :
    ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d), ScalarIdentityGoodTailOnInterval a s 1 m (m + 1) → Book.Ch03.h1EnergyNormOnCube (originCube d (m - 2)) a (finiteAffineSuccessorDifferenceInnerRestriction a m e).toH1 ≤ C * (scalarIdentityCorrectedWeakError a s m + scalarIdentityCorrectedWeakError a s (m + 1)) * euclideanNorm e

    There is a dimension-and-order constant controlling the actual weighted energy of the successive finite affine difference on Q_(m-2). The only coefficient premise is the two-scale unit good-tail bound.