Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch02.Theorems.MultiscaleEllipticity.Finite.SmallTail

Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Finite.SmallTail #

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

Deterministic small-scale tails for q = 1 #

This file records the Ch2 operator-norm version of the deterministic small-tail split at scale zero.

source
theorem HCPolySupport.Book.Ch02.smallTail_geometricWeight_one_nat_add_eq (s : ℝ) (j m : ℕ) :
geometricWeight s 1 (j + m) = Real.rpow 3 (-s * ↑m) * geometricWeight s 1 j

Shift identity for the q = 1 geometric weights in the small-scale tail.

source
theorem HCPolySupport.Book.Ch02.smallTail_exists_descendant_ancestor_at_depth {d : ℕ} {Q R : TriadicCube d} (m n : ℕ) (hR : R ∈ descendantsAtDepth Q (m + n)) :
∃ U ∈ descendantsAtDepth Q m, R ∈ descendantsAtDepth U n

Converse to descendant-depth transitivity: a descendant at depth m + n factors through some depth-m intermediate cube.

source
theorem HCPolySupport.Book.Ch02.smallTail_exists_scale_zero_ancestor_of_mem_descendantsAtScale_originCube_neg_nat {d m j : ℕ} {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d ↑m) (-↑j)) :
∃ U ∈ descendantsAtScale (originCube d ↑m) 0, R ∈ descendantsAtScale U (-↑j)

Every descendant of cu_m at a nonpositive absolute scale -j factors through a scale-zero descendant of cu_m.

source
theorem HCPolySupport.Book.Ch02.coarseBMatrixNorm_le_maxDescendantBMatrixNormAtScale_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) (hR : R ∈ descendantsAtScale Q k) :
coarseBMatrixNorm R a ≤ maxDescendantBMatrixNormAtScale Q k a
source
theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_le_maxDescendantNorm_atScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) (hR : R ∈ descendantsAtScale Q k) :
coarseSigmaStarInvMatrixNorm R a ≤ maxDescendantSigmaStarInvMatrixNormAtScale Q k a
source
theorem HCPolySupport.Book.Ch02.smallTail_tsum_weighted_scale_zero_B_sqrt_tail_eq_LambdaSq_rpow_half {d : ℕ} {U : TriadicCube d} (hUscale : U.scale = 0) (s : ℝ) (m : ℕ) (a : TriadicCoeffFamily d) (hs : 0 ≤ s) :
∑' (j : ℕ), geometricWeight s 1 (j + m) * (maxDescendantBMatrixNormAtScale U (-↑j) a).rpow (1 / 2) = Real.rpow 3 (-s * ↑m) * (LambdaSq U s (MultiscaleExponent.finite 1) a).rpow (1 / 2)

For a fixed scale-zero cube, the small-scale q = 1 square-root tail is exactly the local LambdaSq square-root series times the global scale factor 3^{-sm}.

source
theorem HCPolySupport.Book.Ch02.smallTail_tsum_weighted_scale_zero_sigmaStarInv_sqrt_tail_eq_lambdaSq_rpow_neg_half {d : ℕ} {U : TriadicCube d} (hUscale : U.scale = 0) (s : ℝ) (m : ℕ) (a : TriadicCoeffFamily d) (hs : 0 ≤ s) :
∑' (j : ℕ), geometricWeight s 1 (j + m) * (maxDescendantSigmaStarInvMatrixNormAtScale U (-↑j) a).rpow (1 / 2) = Real.rpow 3 (-s * ↑m) * (lambdaSq U s (MultiscaleExponent.finite 1) a).rpow (-1 / 2)

For a fixed scale-zero cube, the small-scale q = 1 lower inverse square-root tail is exactly the local lambdaSq inverse square-root series times the global scale factor 3^{-sm}.

source
noncomputable def HCPolySupport.Book.Ch02.upperSmallSqrtTail {d : ℕ} (m : ℕ) (s : ℝ) (a : TriadicCoeffFamily d) :
ℝ

The upper small-scale square-root tail after splitting at scale zero.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch02.lowerSmallSqrtTail {d : ℕ} (m : ℕ) (s : ℝ) (a : TriadicCoeffFamily d) :
    ℝ

    The lower inverse small-scale square-root tail after splitting at scale zero.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.Book.Ch02.summable_upperSmallSqrtTail_scale_zero {d : ℕ} [NeZero d] {U : TriadicCube d} (hUscale : U.scale = 0) (m : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      Summable fun (j : ℕ) => geometricWeight s 1 (j + m) * (maxDescendantBMatrixNormAtScale U (-↑j) a).rpow (1 / 2)
      source
      theorem HCPolySupport.Book.Ch02.summable_lowerSmallSqrtTail_scale_zero {d : ℕ} [NeZero d] {U : TriadicCube d} (hUscale : U.scale = 0) (m : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      Summable fun (j : ℕ) => geometricWeight s 1 (j + m) * (maxDescendantSigmaStarInvMatrixNormAtScale U (-↑j) a).rpow (1 / 2)
      source
      theorem HCPolySupport.Book.Ch02.rpow_half_maxDescendantBMatrixNormAtScale_originCube_neg_nat_le_sum_scale_zero {d : ℕ} (m j : ℕ) (a : TriadicCoeffFamily d) :
      (maxDescendantBMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ ∑ U ∈ descendantsAtScale (originCube d ↑m) 0, (maxDescendantBMatrixNormAtScale U (-↑j) a).rpow (1 / 2)

      At a fixed small depth, the upper square-root maximum below cu_m is bounded by summing the corresponding local maxima over the scale-zero descendants of cu_m.

      source
      theorem HCPolySupport.Book.Ch02.rpow_half_maxDescendantSigmaStarInvMatrixNormAtScale_originCube_neg_nat_le_sum_scale_zero {d : ℕ} (m j : ℕ) (a : TriadicCoeffFamily d) :
      (maxDescendantSigmaStarInvMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ ∑ U ∈ descendantsAtScale (originCube d ↑m) 0, (maxDescendantSigmaStarInvMatrixNormAtScale U (-↑j) a).rpow (1 / 2)

      At a fixed small depth, the lower inverse square-root maximum below cu_m is bounded by summing the corresponding local maxima over the scale-zero descendants of cu_m.

      source
      theorem HCPolySupport.Book.Ch02.rpow_half_maxDescendantBMatrixNormAtScale_originCube_neg_nat_le_sup_scale_zero {d : ℕ} (m j : ℕ) (a : TriadicCoeffFamily d) :
      (maxDescendantBMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ (descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) => (maxDescendantBMatrixNormAtScale U (-↑j) a).rpow (1 / 2)

      At a fixed small depth, the upper square-root maximum below cu_m is bounded by the scale-zero supremum of the corresponding local maxima.

      source
      theorem HCPolySupport.Book.Ch02.rpow_half_maxDescendantSigmaStarInvMatrixNormAtScale_originCube_neg_nat_le_sup_scale_zero {d : ℕ} (m j : ℕ) (a : TriadicCoeffFamily d) :
      (maxDescendantSigmaStarInvMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ (descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) => (maxDescendantSigmaStarInvMatrixNormAtScale U (-↑j) a).rpow (1 / 2)

      At a fixed small depth, the lower inverse square-root maximum below cu_m is bounded by the scale-zero supremum of the corresponding local maxima.

      source
      theorem HCPolySupport.Book.Ch02.smallTail_scale_zero_weighted_B_sqrt_le_LambdaSq_rpow_half {d : ℕ} [NeZero d] {U : TriadicCube d} (hUscale : U.scale = 0) {s : ℝ} (hs : 0 < s) (j : ℕ) (a : TriadicCoeffFamily d) :
      geometricWeight s 1 j * (maxDescendantBMatrixNormAtScale U (-↑j) a).rpow (1 / 2) ≤ (LambdaSq U s (MultiscaleExponent.finite 1) a).rpow (1 / 2)
      source
      theorem HCPolySupport.Book.Ch02.smallTail_scale_zero_weighted_sigmaStarInv_sqrt_le_lambdaSq_rpow_neg_half {d : ℕ} [NeZero d] {U : TriadicCube d} (hUscale : U.scale = 0) {s : ℝ} (hs : 0 < s) (j : ℕ) (a : TriadicCoeffFamily d) :
      geometricWeight s 1 j * (maxDescendantSigmaStarInvMatrixNormAtScale U (-↑j) a).rpow (1 / 2) ≤ (lambdaSq U s (MultiscaleExponent.finite 1) a).rpow (-1 / 2)
      source
      theorem HCPolySupport.Book.Ch02.upperSmallSqrtTailTerm_le_scale_factor_mul_scale_zero_LambdaSq_sup'_rpow_half {d : ℕ} [NeZero d] (m j : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      geometricWeight s 1 (j + m) * (maxDescendantBMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ Real.rpow 3 (-s * ↑m) * ((descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) => LambdaSq U s (MultiscaleExponent.finite 1) a).rpow (1 / 2)

      Fixed-scale upper small-tail localization with no scale-zero cardinality loss: the weighted operator-norm square-root term below cu_m is controlled by the scale-zero supremum of LambdaSq.

      source
      theorem HCPolySupport.Book.Ch02.lowerSmallSqrtTailTerm_le_scale_factor_mul_scale_zero_lambdaSq_inv_sup'_rpow_half {d : ℕ} [NeZero d] (m j : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      geometricWeight s 1 (j + m) * (maxDescendantSigmaStarInvMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ Real.rpow 3 (-s * ↑m) * ((descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) => (lambdaSq U s (MultiscaleExponent.finite 1) a)⁻¹).rpow (1 / 2)

      Fixed-scale lower small-tail localization with no scale-zero cardinality loss: the weighted inverse operator-norm square-root term below cu_m is controlled by the scale-zero supremum of lambdaSq⁻¹.

      source
      theorem HCPolySupport.Book.Ch02.upperSmallSqrtTailTerm_sq_le_scale_factor_mul_scale_zero_LambdaSq_sup' {d : ℕ} [NeZero d] (m j : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      (geometricWeight s 1 (j + m) * (maxDescendantBMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2)) ^ 2 ≤ Real.rpow 3 (-s * ↑m) * (descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) => LambdaSq U s (MultiscaleExponent.finite 1) a

      Squared fixed-scale upper small-tail localization with no scale-zero cardinality loss.

      source
      theorem HCPolySupport.Book.Ch02.lowerSmallSqrtTailTerm_sq_le_scale_factor_mul_scale_zero_lambdaSq_inv_sup' {d : ℕ} [NeZero d] (m j : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      (geometricWeight s 1 (j + m) * (maxDescendantSigmaStarInvMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2)) ^ 2 ≤ Real.rpow 3 (-s * ↑m) * (descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) => (lambdaSq U s (MultiscaleExponent.finite 1) a)⁻¹

      Squared fixed-scale lower small-tail localization with no scale-zero cardinality loss.

      source
      theorem HCPolySupport.Book.Ch02.upperSmallSqrtTail_le_scale_factor_mul_sum_scale_zero_LambdaSq_rpow_half {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      upperSmallSqrtTail m s a ≤ Real.rpow 3 (-s * ↑m) * ∑ U ∈ descendantsAtScale (originCube d ↑m) 0, (LambdaSq U s (MultiscaleExponent.finite 1) a).rpow (1 / 2)

      The upper small-scale square-root tail is bounded by the sum of the local scale-zero q = 1 square-root tails, hence by the corresponding scale-zero ellipticity square roots with the global factor 3^{-sm}.

      source
      theorem HCPolySupport.Book.Ch02.lowerSmallSqrtTail_le_scale_factor_mul_sum_scale_zero_lambdaSq_rpow_neg_half {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      lowerSmallSqrtTail m s a ≤ Real.rpow 3 (-s * ↑m) * ∑ U ∈ descendantsAtScale (originCube d ↑m) 0, (lambdaSq U s (MultiscaleExponent.finite 1) a).rpow (-1 / 2)

      The lower inverse small-scale square-root tail is bounded by the sum of the local scale-zero q = 1 inverse square-root tails, hence by the corresponding scale-zero inverse ellipticity square roots with the global factor 3^{-sm}.

      source
      theorem HCPolySupport.Book.Ch02.upperSmallSqrtTail_sq_le_scale_factor_sq_mul_card_sum_scale_zero_LambdaSq {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      upperSmallSqrtTail m s a ^ 2 ≤ Real.rpow 3 (-s * ↑m) ^ 2 * ↑(descendantsAtScale (originCube d ↑m) 0).card * ∑ U ∈ descendantsAtScale (originCube d ↑m) 0, LambdaSq U s (MultiscaleExponent.finite 1) a

      Squared upper small-tail bound using scale-zero LambdaSq values.

      source
      theorem HCPolySupport.Book.Ch02.lowerSmallSqrtTail_sq_le_scale_factor_sq_mul_card_sum_scale_zero_lambdaSq_inv {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : TriadicCoeffFamily d) :
      lowerSmallSqrtTail m s a ^ 2 ≤ Real.rpow 3 (-s * ↑m) ^ 2 * ↑(descendantsAtScale (originCube d ↑m) 0).card * ∑ U ∈ descendantsAtScale (originCube d ↑m) 0, (lambdaSq U s (MultiscaleExponent.finite 1) a)⁻¹

      Squared lower inverse small-tail bound using scale-zero lambdaSq values.