Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.PrintOrderRoundedGenerationResponseRows

High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationResponseRows #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Selected-generation response rows at the printed-order common scale #

The stochastic certificate controls every admissible rounded generation. These definitions retain the selected generation in the physical weak-error row and in the finite good-tail interfaces.

source
noncomputable def HCPolySupport.HighContrast.roundedGenerationSpatialWeakError {d : ℕ} (generation : ℤ) (a : CoeffSpace d) (abar : Mat d) (_hS : Matrix.PosDef (symmPart abar)) (s : ℝ) (M : ℤ) :
ℝ

The full spatial weak error associated with one selected rounded grid.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.roundedGenerationSpatialWeakError_nonneg {d : ℕ} (generation : ℤ) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s : ℝ) (M : ℤ) :
    0 ≤ roundedGenerationSpatialWeakError generation a abar hS s M

    A selected-generation spatial weak error is nonnegative.

    source
    def HCPolySupport.HighContrast.RoundedGenerationSpatialGoodTailOnInterval {d : ℕ} (generation : ℤ) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s delta : ℝ) (n m : ℤ) :
    Prop

    The finite summable response row for a selected rounded generation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def HCPolySupport.HighContrast.RoundedGenerationSpatialGoodTail {d : ℕ} (generation : ℤ) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s delta : ℝ) (n : ℤ) :
      Prop

      The all-later summable response row for a selected rounded generation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def HCPolySupport.HighContrast.RoundedGenerationSpatialGoodMaxOnInterval {d : ℕ} (generation : ℤ) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s delta : ℝ) (n m : ℤ) :
        Prop

        The finite pointwise response row for a selected rounded generation.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.HighContrast.RoundedGenerationSpatialGoodTail.goodMaxOnInterval {d : ℕ} {generation : ℤ} {a : CoeffSpace d} {abar : Mat d} {hS : Matrix.PosDef (symmPart abar)} {s delta : ℝ} {n m : ℤ} (h : RoundedGenerationSpatialGoodTail generation a abar hS s delta n) (hnm : n ≤ m) :
          RoundedGenerationSpatialGoodMaxOnInterval generation a abar hS s delta n m

          A summable selected-generation row controls its pointwise maximum.

          source
          theorem HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.exists_roundedWeakError_le_powerTail {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} {g sourceAmplitude target kappa : ℝ} {X : CoeffSpace d → ℝ} (h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g sourceAmplitude kappa (X a) a) {generation : ℤ} (hl : ↑(kZero d) ≤ generation) (hg : g ∈ Set.Ico 0 1) (hTarget : 0 < target) :
          ∃ (hS : Matrix.PosDef (symmPart abar)), ∀ (M : ℤ), printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a ≤ 3 ^ M → roundedGenerationSpatialWeakError generation a abar hS (printCertificateOrder g) M ≤ target * (3 ^ M / printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a) ^ (-kappa)

          The printed certificate controls the rounded weak error at its corrected common scale.

          source
          theorem HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.exists_roundedGenerationSpatialGoodTail {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} {g sourceAmplitude target kappa : ℝ} {X : CoeffSpace d → ℝ} (h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g sourceAmplitude kappa (X a) a) {generation : ℤ} (hl : ↑(kZero d) ≤ generation) (hg : g ∈ Set.Ico 0 1) (hTarget : 0 < target) :
          ∃ (hS : Matrix.PosDef (symmPart abar)), RoundedGenerationSpatialGoodTail generation a abar hS (printCertificateOrder g) (target / (1 - 3 ^ (-kappa))) ↑(Quenched.triadicCeilingIndex (printOrderCommonQuantitativeAffineScale d g sourceAmplitude target kappa abar X a))

          The printed-order weak errors have a summable all-later tail.