Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.MatrixAverageCompression

Coarse-graining support: #

Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.MatrixAverageCompression

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

source
noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.refinedVarianceBasicBudgetSmallContrastConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
ℝ

The scale-independent small-contrast budget 1 + 4 * M + 8 * M², where M is the pointwise pair-probe budget constant.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedQuadraticProbeAverageRootSqConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (q : FullBlockVec d) :
    ℝ

    The small-contrast constant controlling the squared root bound for a normalized quadratic probe average, including the fourth-power dependence on the probe norm.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedQuadraticProbeAverageUniformRootSqConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      ℝ

      A uniform squared root-bound constant for coordinate and plus/minus quadratic probes, using the common bound 16 on their squared self-pairings.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedMatrixAverageGeometricConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
        ℝ

        The geometric matrix-average budget obtained from the uniform quadratic probe constant by multiplying by 9 and the sixth power of the block-coordinate count.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedQuadraticProbeAverageUniformRootSqConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
          0 ≤ normalizedQuadraticProbeAverageUniformRootSqConst hP4
          source
          theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedMatrixAverageProbeRootBudget_le_card_inv_mul_smallContrastConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) {child parent : ℕ} (hchild_parent : child ≤ parent) :
          normalizedMatrixAverageProbeRootBudget hP hStruct child parent ≤ (↑(descendantsAtScale (originCube d ↑parent) ↑child).card)⁻¹ * normalizedMatrixAverageGeometricConst hP4