Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.Basic

Coarse-graining support: Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.Basic #

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

Basic scalar parameters for the Section 5.4 variance bound #

This file owns the Section 5.4 variance exponent and the elementary scalar weight used in the beta-weighted fluctuation sum.

source
noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBetaCore {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
ℝ

The minimum quantity whose half is the exponent β in the Section 5.4 variance bound at a good scale.

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

    The exponent β used in l.variance.bound.good.scale.homogenization.scale.

    Equations
    Instances For
      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBeta_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      0 < section54VarianceBeta hP4

      The Section 5.4 variance exponent is positive.

      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBeta_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      0 ≤ section54VarianceBeta hP4

      The Section 5.4 variance exponent is nonnegative.

      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBeta_le_sUpper {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      section54VarianceBeta hP4 ≤ hP4.sUpper

      The variance exponent is no larger than the upper regularity exponent.

      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBeta_le_sLower {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      section54VarianceBeta hP4 ≤ hP4.sLower

      The variance exponent is no larger than the lower regularity exponent.

      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBeta_le_sUpper_sub_dim_div_xi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      section54VarianceBeta hP4 ≤ hP4.sUpper - ↑d / ↑hP4.xi

      The variance exponent fits inside the upper positive-excess gain.

      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBeta_le_sLower_sub_dim_div_xi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      section54VarianceBeta hP4 ≤ hP4.sLower - ↑d / ↑hP4.xi

      The variance exponent fits inside the lower positive-excess gain.

      source
      theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBeta_lt_dim_div_two {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      section54VarianceBeta hP4 < ↑d / 2

      The variance exponent is strictly below d / 2, which leaves room in the geometric sums.

      source
      noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceWeight (β : ℝ) (m j : ℕ) :
      ℝ

      The beta weight in the variance bound.

      Equations
      Instances For
        source
        theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceWeight_nonneg (β : ℝ) (m j : ℕ) :
        0 ≤ varianceWeight β m j

        The beta weight is nonnegative.

        source
        @[simp]
        theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceWeight_self (β : ℝ) (m : ℕ) :
        varianceWeight β m m = 1

        At the top scale, the beta weight is one.

        source
        theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceWeight_eq_one_of_le {β : ℝ} {m j : ℕ} (hmj : m ≤ j) :
        varianceWeight β m j = 1

        If j is above m, the Nat-truncated beta weight is one.