Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.Additivity.ParentRestriction

Coarse-graining support: #

Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.Additivity.ParentRestriction

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

AdditivityParentRestriction #

Parent-restricted response identities and the partition defect.

source
noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.castAHarmonicCoeff {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} (h : a = b) (u : AHarmonicFunction a U) :
AHarmonicFunction b U

Transport a harmonic function along an equality of coefficient fields on the same domain.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.castAHarmonicCoeff_grad {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} (h : a = b) (u : AHarmonicFunction a U) :
    (castAHarmonicCoeff h u).toH1.grad = u.toH1.grad
    source
    noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.parentResponseSolutionOnDependentFamilyRestrictedToCube {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
    Ch02.Solution (Ch02.cubeDomain R) ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn R)

    The parent canonical response solution, restricted to a descendant child cube and viewed with the child coefficient representative. For the Chapter 4 dependent family the parent and child coefficient representatives are the same sampled coefficient field, so this needs no representative-identification layer.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.parentResponseSolutionOnDependentFamilyRestrictedToCube_grad {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
      (parentResponseSolutionOnDependentFamilyRestrictedToCube a ha Q hR p q).toH1.grad = canonicalMaximizerGradientOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q

      The restricted parent solution has the parent canonical gradient.

      source
      theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_additivityEnergyDensity_eq_responseJ_sub_parentResponseValue {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
      let F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube F Q R p q) = Ch02.responseJ (Ch02.cubeDomain R) (F.coeffOn R) p q - Ch02.responseValue (Ch02.cubeDomain R) (F.coeffOn R) p q (parentResponseSolutionOnDependentFamilyRestrictedToCube a ha Q hR p q)

      One-child diff-energy identity with the restricted parent solution supplied by the Chapter 4 dependent coefficient family.

      source
      theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.parentRestrictedResponseValueOnDependentFamily_eq_cubeAverage_parentResponseIntegrand {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
      let F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; Ch02.responseValue (Ch02.cubeDomain R) (F.coeffOn R) p q (parentResponseSolutionOnDependentFamilyRestrictedToCube a ha Q hR p q) = cubeAverage R (Ch02.responseIntegrand (Ch02.cubeDomain Q) (F.coeffOn Q) p q (canonicalMaximizerSolutionOnCube Q (F.coeffOn Q) p q))

      The response value of the restricted parent solution on one child cube is the child cube average of the parent response integrand.

      source
      noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.parentRestrictedResponseValueOnDependentFamilyAtDepth {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) :
      TriadicCube d → ℝ

      The descendant-indexed restricted-parent response value.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.parentRestrictedResponseAverage_eq_responseJOnCube {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) :
        have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; descendantsAverage Q j (parentRestrictedResponseValueOnDependentFamilyAtDepth a ha Q j p q) = Ch02.responseJ (Ch02.cubeDomain Q) (F.coeffOn Q) p q

        The descendant average of restricted-parent response values is the parent response.

        source
        theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.descendantMean_additivityHalfEnergy_eq_responseJDefect {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) :
        have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube F Q R p q)) = responseJPartitionDefectOnFamilyAtDepth F Q j p q

        The descendant average of the local difference half-energy is exactly the response partition defect for the Chapter 4 dependent coefficient family.