Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.ABK26.LocalCoarseGrainingResponse

Coarse-graining support: Support.Book.Ch03.ABK26.LocalCoarseGrainingResponse #

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

source
noncomputable def HCPolySupport.Book.Ch03.ABK26.rootPointwiseCoeffFamily {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) :
Ch02.TriadicCoeffFamily d

The globally measurable pointwise-good representative of a root coefficient, viewed as a compatible coefficient family on every triadic cube.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Book.Ch03.ABK26.rootPointwiseCoeffFamily_root_aeeq {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) :
    ((rootPointwiseCoeffFamily Q a).coeffOn Q).AEEq a

    At its root, the canonical pointwise family agrees a.e. with the supplied public coefficient.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.rootPointwiseCoeffFamily_descendant_aeeq {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) {R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) :
    ((rootPointwiseCoeffFamily Q a).coeffOn R).AEEq (a.restrictToSubcube ⋯)

    On every descendant, the canonical pointwise family agrees a.e. with the literal restriction of the supplied root coefficient.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.normalizedBlockResponseScalarEMaxOnCube_le_ofReal_rootPointwise {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) {R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) :
    Ch02.normalizedBlockResponseScalarEMaxOnCube R (a.restrictToSubcube ⋯) sigma0 hsigma0 ≤ ENNReal.ofReal (Ch02.normalizedBlockResponseMax R (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0))

    On a descendant, the canonical extended-real scalar response maximum is no larger than the nonnegative encoding of the legacy real response maximum.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.ofReal_normalizedBlockResponseMax_le_rootPointwise {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) {R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) :
    ENNReal.ofReal (Ch02.normalizedBlockResponseMax R (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0)) ≤ Ch02.normalizedBlockResponseScalarEMaxOnCube R (a.restrictToSubcube ⋯) sigma0 hsigma0

    Conversely, the nonnegative encoding of the legacy real response maximum is bounded by the canonical extended-real scalar response maximum.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.normalizedBlockResponseScalarEMaxOnCube_eq_ofReal_rootPointwise {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) {R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) :
    Ch02.normalizedBlockResponseScalarEMaxOnCube R (a.restrictToSubcube ⋯) sigma0 hsigma0 = ENNReal.ofReal (Ch02.normalizedBlockResponseMax R (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0))

    The real and extended-real one-cube response maxima agree exactly for the canonical root family and every descendant of its root.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.parentTruncatedNormalizedBlockResponseScalarEMaxAtScale_eq_ofReal {d : ℕ} [NeZero d] (Q : TriadicCube d) (k : ℤ) (hk : k ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) :
    Ch02.parentTruncatedNormalizedBlockResponseScalarEMaxAtScale Q k hk a sigma0 hsigma0 = ENNReal.ofReal (Ch02.maxDescendantNormalizedBlockResponseAtScale Q k (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0))

    At every physical scale, the canonical parent extended-real maximum is the nonnegative encoding of the legacy finite descendant maximum for the root pointwise family.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.parentTruncatedHomogenizationErrorInfinityOneScalar_eq_ofReal {d : ℕ} [NeZero d] (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s : ↑FractionalOrder) :
    Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s = ENNReal.ofReal (Ch02.HomogenizationErrorFinite Q n (↑s) Ch02.MultiscaleExponent.infinity 1 (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0))

    The canonical frozen q = 1 parent error is exactly the extended-real encoding of the legacy finite homogenization error for the root family.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.parentTruncatedHomogenizationErrorInfinityTwoScalar_eq_ofReal {d : ℕ} [NeZero d] (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s : ↑FractionalOrder) :
    Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s = ENNReal.ofReal (Ch02.HomogenizationErrorFinite Q n (↑s) Ch02.MultiscaleExponent.infinity 2 (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0))

    The canonical frozen q = 2 parent error is exactly the extended-real encoding of the legacy finite homogenization error for the root family.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.rootPointwise_scaleResponse_shift_le {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) {R : TriadicCube d} {k : ℤ} (hkn : k ≤ n) (hR : R ∈ descendantsAtScale Q k) (j : ℕ) :
    Ch02.scaleResponseAtScale R (R.scale - ↑j) Ch02.MultiscaleExponent.infinity (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0) ≤ Ch02.scaleResponseAtScale Q (n - ↑(j + (n - k).toNat)) Ch02.MultiscaleExponent.infinity (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0)

    The one-scale response comparison used in the exact shifted parent-error series. A descendant's on-cube term at depth j is controlled by the root family at the matching physical scale n - (h + j).

    source
    theorem HCPolySupport.Book.Ch03.ABK26.summable_rootPointwise_descendant_infinity_one_terms {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) {R : TriadicCube d} {k : ℤ} (_hR : R ∈ descendantsAtScale Q k) (sigma0 : ℝ) (s : ↑FractionalOrder) :
    Summable fun (j : ℕ) => Ch02.geometricWeight (↑s) 1 j * Ch02.scaleResponseAtScale R (R.scale - ↑j) Ch02.MultiscaleExponent.infinity (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0)

    The source-family-facing on-cube q = 1 response series is summable on every descendant.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.rootPointwise_descendant_infinity_one_le_parent {d : ℕ} [NeZero d] (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) {R : TriadicCube d} {k : ℤ} (hkn : k ≤ n) (hR : R ∈ descendantsAtScale Q k) (s : ↑FractionalOrder) :
    ENNReal.ofReal (Ch02.HomogenizationErrorOnCube R (↑s) Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 1) (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0)) ≤ ENNReal.ofReal (Real.rpow 3 (↑s * ↑(n - k).toNat)) * Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s

    Exact shifted localization of a descendant on-cube q = 1 error by the canonical parent-truncated error.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.rootPointwise_descendant_infinity_two_le_parent {d : ℕ} [NeZero d] (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) {R : TriadicCube d} {k : ℤ} (hkn : k ≤ n) (hR : R ∈ descendantsAtScale Q k) (s : ↑FractionalOrder) :
    ENNReal.ofReal (Ch02.HomogenizationErrorOnCube R (↑s) Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 2) (rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0)) ≤ ENNReal.ofReal (Real.rpow 3 (↑s * ↑(n - k).toNat)) * Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s

    Exact shifted localization of a descendant on-cube q = 2 error by the canonical parent-truncated error.