Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section53.WeakNormsMaximizer.EnergyDefect

Coarse-graining support: Support.Book.Ch05.Theorems.Section53.WeakNormsMaximizer.EnergyDefect #

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

Response-defect identifications for the weak-norm maximizer lemma #

This file connects the defect term used in the second Section 5.3 lemma to the deterministic response partition defect already developed for the first Section 5.3 lemma.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.descendantMean_responseJObservableSet_sub_eq_responseJPartitionDefect {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) :
(descendantsAverage Q j fun (R : TriadicCube d) => Ch04.restrictionResponseJObservableCubeSet R p q a) - Ch04.restrictionResponseJObservableCubeSet Q p q a = JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) Q j p q

For the Ch4 dependent coefficient family, the descendant average of Ch4 response observables minus the parent response is the raw deterministic partition defect.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.responseDefectAverageAtScale_eq_responseJPartitionDefectOnDependentFamily {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m n : ℤ) (p q : Vec d) :
responseDefectAverageAtScale m n p q a = JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (originCube d m) (m - n).toNat p q

The scale-indexed defect in the weak-norm maximizer RHS is the deterministic response partition defect for the dependent coefficient family.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.responseJPartitionDefectOnFamilyAtDepth_nonneg {d : ℕ} (F : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) :
0 ≤ JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p q

Deterministic nonnegativity of the raw response partition defect.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.responseDefectAverageAtScale_nonneg_of_aelocallyUniformlyEllipticField {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m n : ℤ) (p q : Vec d) :
0 ≤ responseDefectAverageAtScale m n p q a

Deterministic nonnegativity of the weak-norm maximizer response-defect term on the a.e.-elliptic support.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.cubeAverageVec_parentChildCanonicalGradientMismatchOnDependentFamily_eq_ch04 {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; (cubeAverageVec R fun (x : Vec d) => JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube Q (F.coeffOn Q) p q x - JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube R (F.coeffOn R) p q x) = Ch04.canonicalScalarResponseGradientAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseGradientAverageCubeSet R R p q a.toFun

The Ch4 gradient average mismatch is the cube average of the raw parent-minus-child canonical maximizer gradients.

source
theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.cubeAverageVec_parentChildCanonicalFluxMismatchOnDependentFamily_eq_ch04 {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; (cubeAverageVec R fun (x : Vec d) => JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube Q (F.coeffOn Q) p q x - JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube R (F.coeffOn R) p q x) = Ch04.canonicalScalarResponseFluxAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseFluxAverageCubeSet R R p q a.toFun

The Ch4 flux average mismatch is the cube average of the raw parent-minus-child canonical maximizer fluxes.

source
noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.parentChildCanonicalDifferenceSolutionOnDependentFamily {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-child canonical difference as an honest Chapter 2 solution on the child cube. This is the deterministic object whose variation energy is the additivity defect.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.parentChildCanonicalDifferenceSolutionOnDependentFamily_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) :
    (parentChildCanonicalDifferenceSolutionOnDependentFamily a ha Q hR p q).toH1.grad = fun (x : Vec d) => JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x - JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube R ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn R) p q x

    The gradient of the parent-child difference solution is the raw parent-minus-child canonical maximizer gradient.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.averageGradient_parentChildCanonicalDifferenceSolutionOnDependentFamily_eq_cubeAverageVec {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.averageGradient (Ch02.cubeDomain R) (F.coeffOn R) (parentChildCanonicalDifferenceSolutionOnDependentFamily a ha Q hR p q) = cubeAverageVec R fun (x : Vec d) => JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube Q (F.coeffOn Q) p q x - JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube R (F.coeffOn R) p q x

    The averaged gradient of the parent-child difference solution is the raw parent-minus-child gradient cube average.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.averageFlux_parentChildCanonicalDifferenceSolutionOnDependentFamily_eq_cubeAverageVec {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.averageFlux (Ch02.cubeDomain R) (F.coeffOn R) (parentChildCanonicalDifferenceSolutionOnDependentFamily a ha Q hR p q) = cubeAverageVec R fun (x : Vec d) => JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube Q (F.coeffOn Q) p q x - JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube R (F.coeffOn R) p q x

    The averaged flux of the parent-child difference solution is the raw parent-minus-child flux cube average.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.variationEnergyValue_parentChildCanonicalDifferenceSolutionOnDependentFamily_eq {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.variationEnergyValue (Ch02.cubeDomain R) (F.coeffOn R) (parentChildCanonicalDifferenceSolutionOnDependentFamily a ha Q hR p q) = 2 * cubeAverage R (JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube F Q R p q)

    The variation energy of the parent-child difference solution is twice the local additivity half-energy.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.vecNormSq_cubeAverageVec_parentChildCanonicalGradientMismatchOnDependentFamily_le {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
    have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; vecNormSq (cubeAverageVec R fun (x : Vec d) => JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube Q (F.coeffOn Q) p q x - JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube R (F.coeffOn R) p q x) ≤ 2 * Ch02.coarseSigmaStarInvMatrixNorm R F * cubeAverage R (JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube F Q R p q)

    One-child averaged parent-child gradient mismatch is controlled by the local σ_*^{-1} norm and the additivity defect energy.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.vecNormSq_cubeAverageVec_parentChildCanonicalFluxMismatchOnDependentFamily_le {d : ℕ} (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
    have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; vecNormSq (cubeAverageVec R fun (x : Vec d) => JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube Q (F.coeffOn Q) p q x - JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube R (F.coeffOn R) p q x) ≤ 2 * Ch02.coarseBMatrixNorm R F * cubeAverage R (JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube F Q R p q)

    One-child averaged parent-child flux mismatch is controlled by the local b norm and the additivity defect energy.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.descendantsAverage_ch04GradientMismatch_le_maxSigmaStarInv_mul_responseDefect {d : ℕ} [NeZero 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) => vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseGradientAverageCubeSet R R p q a.toFun)) ≤ 2 * Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑j) F * JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p q

    At one depth, the Ch4 gradient parent-child mismatch average is controlled by the max descendant σ_*^{-1} norm and the response partition defect.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.descendantsAverage_ch04FluxMismatch_le_maxB_mul_responseDefect {d : ℕ} [NeZero 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) => vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseFluxAverageCubeSet R R p q a.toFun)) ≤ 2 * Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑j) F * JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p q

    At one depth, the Ch4 flux parent-child mismatch average is controlled by the max descendant b norm and the response partition defect.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.sqrt_gradientMismatchAverage_le_two_sqrt_maxInv_mul_sqrt_defect {d : ℕ} [NeZero 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) => vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseGradientAverageCubeSet R R p q a.toFun)) ≤ 2 * √(Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑j) F) * √(JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p q)

    Square-root form of the depth-j gradient mismatch estimate.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.sqrt_descendantsAverage_ch04FluxMismatch_le_two_mul_sqrt_maxB_mul_sqrt_responseDefect {d : ℕ} [NeZero 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) => vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseFluxAverageCubeSet R R p q a.toFun)) ≤ 2 * √(Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑j) F) * √(JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p q)

    Square-root form of the depth-j flux mismatch estimate.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.descendantsAverage_ch04GradientMismatch_le_lambdaSqCoeffField_responseDefect {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) {s' : ℝ} (hs' : 0 < s') (p q : Vec d) :
    have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; (descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseGradientAverageCubeSet R R p q a.toFun)) ≤ (2 * √(Ch04.lambdaSqCoeffField Q s' (Ch02.MultiscaleExponent.finite 1) a)⁻¹ * Real.rpow 3 (s' * ↑j)) ^ 2 * JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p q

    Depth-j gradient mismatch localized by the q=1 lower ellipticity observable on the parent cube.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.descendantsAverage_ch04FluxMismatch_le_LambdaSqCoeffField_responseDefect {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) {t' : ℝ} (ht' : 0 < t') (p q : Vec d) :
    have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; (descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseFluxAverageCubeSet R R p q a.toFun)) ≤ (2 * √(Ch04.LambdaSqCoeffField Q t' (Ch02.MultiscaleExponent.finite 1) a) * Real.rpow 3 (t' * ↑j)) ^ 2 * JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth F Q j p q

    Depth-j flux mismatch localized by the q=1 upper ellipticity observable on the parent cube.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.gradientHighMismatchSum_le_lambdaSqCoeffField_responseDefectSum {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (N : ℕ) (high : ℕ → Prop) [DecidablePred high] {s s' : ℝ} (hs' : 0 < s') (p q : Vec d) :
    ∑ j ∈ Finset.range (N + 1) with high j, Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseGradientAverageCubeSet R R p q a.toFun)) ≤ 2 * √(Ch04.lambdaSqCoeffField Q s' (Ch02.MultiscaleExponent.finite 1) a)⁻¹ * ∑ j ∈ Finset.range (N + 1) with high j, Real.rpow 3 (-(s - s') * ↑j) * √(JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) Q j p q)

    Finite high-depth gradient mismatch sum localized by the q=1 lower ellipticity observable and the response partition defect.

    source
    theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.fluxHighMismatchSum_le_LambdaSqCoeffField_responseDefectSum {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (N : ℕ) (high : ℕ → Prop) [DecidablePred high] {t t' : ℝ} (ht' : 0 < t') (p q : Vec d) :
    ∑ j ∈ Finset.range (N + 1) with high j, Real.rpow 3 (-t * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet Q R p q a.toFun - Ch04.canonicalScalarResponseFluxAverageCubeSet R R p q a.toFun)) ≤ 2 * √(Ch04.LambdaSqCoeffField Q t' (Ch02.MultiscaleExponent.finite 1) a) * ∑ j ∈ Finset.range (N + 1) with high j, Real.rpow 3 (-(t - t') * ↑j) * √(JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) Q j p q)

    Finite high-depth flux mismatch sum localized by the q=1 upper ellipticity observable and the response partition defect.